From a669a6fb68902a515d2c0176e9eb93faf4075f6b Mon Sep 17 00:00:00 2001
From: Sylvie Boldo <sylvie.boldo@inria.fr>
Date: Wed, 31 Jan 2024 22:05:14 +0100
Subject: [PATCH] Preuve injS_equiv_seq

---
 FEM/Algebra/ord_compl.v | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 9d8e16d4..99d96f0e 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -125,14 +125,15 @@ Proof.
 intros P sT f; split.
 (* *)
 intros H s Hs x y Hx Hy; apply H.
-admit.
-admit.
+generalize Hx; apply /allP; easy.
+generalize Hy; apply /allP; easy.
 (* *)
 intros H x y Hx Hy; apply (H [:: x; y]).
-
-
-
-Admitted.
+apply /all_filterP; simpl.
+rewrite Hx Hy; easy.
+rewrite in_cons eq_refl; easy.
+rewrite in_cons mem_seq1 eq_refl; apply orbT.
+Qed.
 
 End Seq_compl2.
 
-- 
GitLab