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

---
 src/permutations.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/permutations.v b/src/permutations.v
index 1c6663e..78d4d88 100644
--- a/src/permutations.v
+++ b/src/permutations.v
@@ -155,6 +155,7 @@ Lemma perm_max_insert : forall (l1 l2: list nat),
   permutation (l1 ++ l2) <-> permutation (l1 ++ [ length (l1++l2) ] ++ l2).
 Proof.
   intros l1 l2. split; intro H.
+  (* first part of the proof *)
   unfold permutation. intro k. intro I.
   rewrite app_length in I. simpl in I. rewrite Nat.add_succ_r in I.
   rewrite Nat.lt_succ_r in I. rewrite <- app_length in I.
@@ -163,6 +164,7 @@ Proof.
   assumption. rewrite in_app_iff. right. apply in_cons. assumption.
   rewrite <- H0. rewrite in_app_iff. right. apply in_eq.
 
+  (* second part of the 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.
@@ -184,7 +186,6 @@ Proof.
   rewrite Nat.add_succ_r in H. rewrite seq_S in H. apply incl_app_inv in H.
   destruct H. rewrite app_length at 1. assumption.
   easy. apply Add_app.
-
   unfold incl in I. unfold permutation.
   intro k. intro. apply I. apply in_seq.
   split. apply Nat.le_0_l. assumption.