From 9f6ac320f9d60ba0d03b8aa6a9feae74bd1cccbc Mon Sep 17 00:00:00 2001
From: Sylvie Boldo <sylvie.boldo@inria.fr>
Date: Tue, 11 Mar 2025 15:46:41 +0100
Subject: [PATCH] Missing lemma inj_ASdki_incr

---
 Algebra/Monoid/Monomial_order.v | 48 +++++++++++++++++++++++++++++++++
 FEM/multi_index.v               | 12 +++++----
 2 files changed, 55 insertions(+), 5 deletions(-)

diff --git a/Algebra/Monoid/Monomial_order.v b/Algebra/Monoid/Monomial_order.v
index c9a87323..aff6ecc4 100644
--- a/Algebra/Monoid/Monomial_order.v
+++ b/Algebra/Monoid/Monomial_order.v
@@ -1873,6 +1873,54 @@ apply graded_br_plus_compat_l; try easy.
 apply symlex_br_plus_compat_l; easy.
 Qed.
 
+Lemma lex_insertF : forall R {n} i t (x y:'G^n),
+   irreflexive R ->
+   lex R x y -> lex R (insertF i t x) (insertF i t y).
+Proof.
+intros R; induction n.
+intros i t x y K H1; contradict H1.
+replace x with y by now apply hat0F_unit.
+apply lex_irrefl; easy.
+intros i t x y K H1.
+case (ord_eq_dec i ord0); intros Hi.
+rewrite Hi lex_irrefl_S; try easy.
+right; split.
+rewrite insertF_correct_l; try easy.
+rewrite insertF_correct_l; easy.
+rewrite 2!skipF_insertF; easy.
+rewrite lex_irrefl_S in H1; try easy; case H1.
+intros H2.
+rewrite lex_irrefl_S; try easy; left.
+rewrite insertF_correct_r; try easy.
+intros Hi'; rewrite insertF_correct_r; try easy.
+rewrite insert_ord_0; easy.
+intros (H2,H3).
+rewrite lex_irrefl_S; try easy; right; split.
+rewrite insertF_correct_r; try easy.
+intros Hi'; rewrite insertF_correct_r; try easy.
+rewrite insert_ord_0; easy.
+rewrite skipF_insertF_comm; try easy.
+intros Hi'.
+rewrite skipF_insertF_comm; try easy.
+apply IHn; try easy.
+rewrite insert_ord_0; easy.
+Qed.
+
+Lemma grsymlex_insertF : forall R {n} i t (x y:'G^n),
+  irreflexive R -> br_plus_compat_l R ->
+   grsymlex R x y -> grsymlex R (insertF i t x) (insertF i t y).
+Proof.
+intros R n i t x y K0 K1 H1; case H1; clear H1.
+intros (H2,H3); apply graded_irrefl_l; try easy.
+rewrite 2!sum_insertF.
+apply K1; easy.
+intros (H2,H3).
+right; split.
+rewrite 2!sum_insertF; f_equal; easy.
+apply lex_insertF; easy.
+Qed.
+
+
 
 
 End Graded_lex_order_Facts1.
diff --git a/FEM/multi_index.v b/FEM/multi_index.v
index 585b07ab..c4b30707 100644
--- a/FEM/multi_index.v
+++ b/FEM/multi_index.v
@@ -672,15 +672,17 @@ rewrite 2!skipF_insertF.
 apply Adk_sortedF; easy.
 Qed.
 
-(* TODO est-ce vrai ??
+
 Lemma inj_ASdki_incr : forall j (idk1 idk2 : 'I_(pbinom d k).+1), 
    (idk1 < idk2)%coq_nat ->
       grsymlex_lt (inj_ASdki j idk1) (inj_ASdki j idk2).
 Proof.
-intros j idk1 idk2 H1.
-unfold inj_ASdki.
-Admitted.
-*)
+intros j idk1 idk2 H1; unfold inj_ASdki.
+apply grsymlex_insertF.
+intros x; apply Nat.lt_irrefl.
+apply lt_plus_compat_l.
+apply Adk_sortedF; easy.
+Qed.
 
 
 End Injection_Facts.
-- 
GitLab