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 07:53:51 +02:00
parent 69549d5bfa
commit a949320a6f
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/permutations.v
View File

@ -130,8 +130,13 @@ Lemma perm_eq : forall (l1 l2: list nat),
-> incl l1 l2 /\ incl l2 l1. -> incl l1 l2 /\ incl l2 l1.
Proof. Proof.
intros l1 l2. intros H I J. intros l1 l2. intros H I J.
Admitted. assert (K1 := H). assert (K2 := H). assert (K3 := I). assert (K4 := I).
apply perm_seq_1 in K1. apply perm_seq_2 in K2.
apply perm_seq_1 in K3. apply perm_seq_2 in K4.
rewrite J in K1. rewrite J in K2.
split. apply incl_tran with (m := seq 0 (length l2)); assumption.
apply incl_tran with (m := seq 0 (length l2)); assumption.
Qed.
Lemma perm_incl : forall (l1 l2: list nat), Lemma perm_incl : forall (l1 l2: list nat),