From e561abd3183952cf9863de958e6923e471aae427 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sat, 21 Oct 2023 15:52:23 +0200
Subject: [PATCH] Update

---
 src/permutations.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/permutations.v b/src/permutations.v
index 5b7bca9..58ed803 100644
--- a/src/permutations.v
+++ b/src/permutations.v
@@ -97,7 +97,6 @@ Proof.
 Qed.
 
 
-
 Lemma perm_max : forall (l: list nat),
   permutation l -> l <> nil -> In (length l - 1) l.
 Proof.
@@ -151,6 +150,7 @@ Proof.
   assumption. destruct l. contradiction I. reflexivity. easy.
 Qed.
 
+
 Lemma perm_max_insert : forall (l1 l2: list nat),
   permutation (l1 ++ l2) <-> permutation (l1 ++ [ length (l1++l2) ] ++ l2).
 Proof.
@@ -168,8 +168,8 @@ Proof.
   assert (I: incl (seq 0 (length (l1++l2))) (l1++l2)).
   assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)).
   unfold incl. intro a. intro J. rewrite app_assoc in J.
-  rewrite in_app_iff. rewrite in_app_iff in J. destruct J.
-  right. assumption. left. assumption. apply incl_app_inv in H0.
+  rewrite in_app_iff. rewrite in_app_iff in J.
+  destruct J ; [ right | left ]; assumption. apply incl_app_inv in H0.
   destruct H0. apply incl_app_inv in H1. destruct H1.
   assert (incl (l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)).
   apply incl_app; assumption.
@@ -177,9 +177,9 @@ Proof.
   apply incl_app; assumption.
   apply incl_Add_inv
       with (a := length (l1++l2)) (v := l1++[length (l1++l2)]++l2).
-  rewrite in_seq. lia. (* TODO *)
+  rewrite in_seq. lia.
   replace (length (l1 ++ l2) :: seq 0 (length (l1 ++ l2)))
-    with ([length (l1 ++ l2)] ++ seq 0 (length (l1 ++ l2))).
+      with ([length (l1 ++ l2)] ++ seq 0 (length (l1 ++ l2))).
   apply incl_app. easy.
   apply perm_seq_1 in H. rewrite app_length in H. simpl in H.
   rewrite Nat.add_succ_r in H. rewrite seq_S in H. apply incl_app_inv in H.