From 68ae96eba58442c6b30ce0f28fcf22e534df013c 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 11:47:24 +0100
Subject: [PATCH] Remove wrong statement!
---
FEM/Algebra/ord_compl.v | 10 ----------
1 file changed, 10 deletions(-)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 7e2aeb94..5e210042 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -2576,14 +2576,4 @@ replace (size _) with (lenPF (fun i => P (widen_S i)));
unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
Qed.
-(* FC (19/12/2023): check this statement!
-Lemma filterP_rev_ord :
- forall {n} {P : 'I_n -> Prop},
- filterP_ord \o (@rev_ord (lenPF P)) = @rev_ord n \o filterP_ord.
-Proof.
-intros n P; apply fun_ext; intros j.
-rewrite !comp_correct. unfold filterP_ord.
-apply ord_inj. simpl.
-Aglopted.*)
-
End FilterP_ord.
--
GitLab