Update

2023-10-22 18:02:20 +02:00 · 2023-10-22 18:02:20 +02:00 · 4373d958b2
commit 4373d958b2
parent a3bf33c2d0
1 changed files with 1 additions and 2 deletions
--- a/src/permutations.v
+++ b/src/permutations.v
@ -208,8 +208,7 @@ Qed.


 Lemma perm_max_insert_alt_2 : forall (l1 l2: list nat),
-  Add (length l1) l1 l2 -> permutation l2
-  -> permutation l1.
+  Add (length l1) l1 l2 -> permutation l2 -> permutation l1.
 Proof.
  intros l1 l2. intros H I.
  apply Add_split in H. destruct H. destruct H. destruct H.