From a949320a6f343406dfb1003508d15c6007648c6b Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 21 Oct 2023 07:53:51 +0200 Subject: [PATCH] Update --- src/permutations.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/permutations.v b/src/permutations.v index 2c27461..c10422b 100644 --- a/src/permutations.v +++ b/src/permutations.v @@ -130,8 +130,13 @@ Lemma perm_eq : forall (l1 l2: list nat), -> incl l1 l2 /\ incl l2 l1. Proof. 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),