diff --git a/src/permutations.v b/src/permutations.v
index 7eb0530..1c6663e 100644
--- a/src/permutations.v
+++ b/src/permutations.v
@@ -152,10 +152,9 @@ Proof.
 Qed.
 
 Lemma perm_max_insert : forall (l1 l2: list nat),
-  permutation (l1 ++ l2) -> permutation (l1 ++ [ length (l1++l2) ] ++ l2).
+  permutation (l1 ++ l2) <-> permutation (l1 ++ [ length (l1++l2) ] ++ l2).
 Proof.
-  intros l1 l2. intro H.
-  (* first part of the proof *)
+  intros l1 l2. split; intro H.
   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,12 +162,6 @@ Proof.
   apply in_app_iff in H0. destruct H0. rewrite in_app_iff. left.
   assumption. rewrite in_app_iff. right. apply in_cons. assumption.
   rewrite <- H0. rewrite in_app_iff. right. apply in_eq.
-Qed.
-
-Lemma perm_max_insert_alt : forall (l1 l2: list nat),
-  permutation (l1 ++ [ length (l1++l2) ] ++ l2) -> permutation (l1 ++ l2).
-Proof.
-  intros l1 l2. intro H.
 
   assert (I: incl (seq 0 (length (l1++l2))) (l1++l2)).
   assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)).
@@ -193,7 +186,8 @@ Proof.
   easy. apply Add_app.
 
   unfold incl in I. unfold permutation.
-  intro k. intro. apply I. apply in_seq. lia. (* TODO *)
+  intro k. intro. apply I. apply in_seq.
+  split. apply Nat.le_0_l. assumption.
 Qed.