From c9b76db041eb000a0bceb7e1a4f5ec060dfe7169 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 5 Feb 2024 19:12:30 +0100
Subject: [PATCH] WIP: simpler proof of filterP_ord_ind_l_in_n0.
---
FEM/Algebra/ord_compl.v | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 38959363..d3a0e855 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -2527,6 +2527,14 @@ Lemma filterP_ord_ind_l_in_n0 :
(j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_l_in HP) j <> ord0),
filterP_ord j = lift_S (filterP_ord (lower_S Hj)).
Proof.
+(*
+intros n P HP j Hj1.
+assert (Hj2 :
+ (filterP_ord (Ordinal (lenPF_n0_rev HP)) < filterP_ord j)%coq_nat).
+ apply filterP_ord_incrF; rewrite -(cast_ord_n0_equiv_gt ); apply Hj1.
+rewrite (filterP_ord_ind_l_in_0 ) in Hj2; [| apply ord_inj; easy].
+*)
+
intros n P HP j Hj; destruct n as [| n].
(* *)
exfalso; destruct (le_1_dec (lenPF_le P)) as [HP' | HP'].
--
GitLab