baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-10-21 17:05:42 +02:00
parent ec3c0fb335
commit 4908dae055
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/permutations.v
View File

@ -190,7 +190,7 @@ Qed.
Lemma perm_max_insert_alt : forall (l1 l2: list nat),
permutation l1 -> (Add (length l1) l1 l2 -> permutation l2).
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.