Update
This commit is contained in:
parent
e561abd318
commit
ec3c0fb335
@ -189,6 +189,17 @@ Proof.
|
|||||||
Qed.
|
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.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user