From ec3c0fb335c8a10b46248a66169688a23787f3c1 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 21 Oct 2023 16:57:55 +0200 Subject: [PATCH] Update --- src/permutations.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/permutations.v b/src/permutations.v index 58ed803..550ade7 100644 --- a/src/permutations.v +++ b/src/permutations.v @@ -189,6 +189,17 @@ Proof. Qed. +Lemma perm_max_insert_alt : forall (l1 l2: list nat), + permutation l1 -> (Add (length l1) l1 l2 -> permutation l2). +Proof. + intros l1 l2. intros H I. + apply Add_split in I. destruct I. destruct H0. destruct H0. + rewrite H0 in H. rewrite H1. rewrite H0. + replace (length (x++x0) :: x0) with ([length (x++x0)] ++ x0). + rewrite <- perm_max_insert. assumption. easy. +Qed. + +