diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index edf1f9fbe7f522816c17307d34b0c50d234eb19d..e57b68ad1f016d64da545eb3e818abe32e221c2b 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -16,7 +16,53 @@ Notation "''' E ^ n" := ('I_n -> E)
   (at level 8, E at level 2, n at level 2, format "''' E ^ n").
 
 
-Section FF_Def0.
+Section FF_Def0a.
+
+Context {n : nat}.
+Variable P Q : 'Prop^n.
+
+(* The prefix "P" stands for Prop, "A" for "forall", "E" for "exists". *)
+Definition PAF : Prop := forall i, P i.
+Definition PEF : Prop := exists i, P i.
+
+Definition notF : 'Prop^n := fun i => ~ P i. (* = compl P. *)
+Definition andF : 'Prop^n := fun i => P i /\ Q i. (* = inter P Q. *)
+Definition orF : 'Prop^n := fun i => P i \/ Q i. (* = union P Q. *)
+Definition impF : 'Prop^n := fun i => P i -> Q i.
+Definition equivF : 'Prop^n := fun i => P i <-> Q i.
+
+End FF_Def0a.
+
+
+Section FF_Def1a.
+
+Context {n : nat}.
+Variable P : 'Prop^n.
+
+Lemma PF_dec : {PAF P} + {PEF (notF P)}.
+Proof.
+destruct (excluded_middle_informative (PAF P));
+    [left | right; apply not_all_ex_not_equiv]; easy.
+Qed.
+
+Lemma PF_dec_l : forall (H : PAF P), PF_dec = left H.
+Proof.
+intros H1; destruct PF_dec as [H2 | H2].
+f_equal; apply proof_irrelevance.
+contradict H1; apply not_all_ex_not_equiv; easy.
+Qed.
+
+Lemma PF_dec_r : forall (H : PEF (notF P)), PF_dec = right H.
+Proof.
+intros H1; destruct PF_dec as [H2 | H2].
+contradict H2; apply not_all_ex_not_equiv; easy.
+f_equal; apply proof_irrelevance.
+Qed.
+
+End FF_Def1a.
+
+
+Section FF_Def0b.
 
 Context {E : Type}.
 Variable R : E -> E -> Prop.
@@ -24,11 +70,11 @@ Variable R : E -> E -> Prop.
 Context {n : nat}.
 Variable A B : 'E^n.
 
-(* "br" stands for "binary relation", "A" for "forall", "E" for "exists". *)
-Definition brAF : Prop := forall i, R (A i) (B i).
-Definition brEF : Prop := exists i, R (A i) (B i).
+(* The prefix "br" stands for "binary relation". *)
+Definition brAF : Prop := PAF (fun i => R (A i) (B i)).
+Definition brEF : Prop := PEF (fun i => R (A i) (B i)).
 
-End FF_Def0.
+End FF_Def0b.
 
 
 Section FF_Def1.
@@ -39,29 +85,14 @@ Variable R : E -> E -> Prop.
 Context {n : nat}.
 Variable A B : 'E^n.
 
-Lemma brF_dec : {brAF R A B} + {brEF (br_not R) A B}.
-Proof.
-destruct (excluded_middle_informative (brAF R A B));
-    [left | right; apply not_all_ex_not_equiv]; easy.
-Qed.
+Definition brF_dec : {brAF R A B} + {brEF (br_not R) A B} :=
+  PF_dec (fun i => R (A i) (B i)).
 
-Lemma brF_dec_l : forall (H:brAF R A B), brF_dec = left H.
-Proof.
-intros H; case brF_dec; try easy.
-intros H'; f_equal.
-apply proof_irrelevance.
-intros H1; contradict H.
-apply not_all_ex_not_equiv, H1.
-Qed.
+Lemma brF_dec_l : forall (H : brAF R A B), brF_dec = left H.
+Proof. intros; apply PF_dec_l. Qed.
 
-Lemma brF_dec_r : forall (H:brEF (br_not R) A B), brF_dec = right H.
-Proof.
-intros H; case brF_dec; try easy.
-intros H1; contradict H1.
-apply not_all_ex_not_equiv, H.
-intros H'; f_equal.
-apply proof_irrelevance.
-Qed.
+Lemma brF_dec_r : forall (H : brEF (br_not R) A B), brF_dec = right H.
+Proof. intros; apply PF_dec_r. Qed.
 
 Definition eqAF : Prop := brAF eq A B.
 Definition eqEF : Prop := brEF eq A B.
@@ -112,7 +143,7 @@ Context {n : nat}.
 Variable f g : '(E -> F)^n.
 
 Lemma fun_extF : same_funF f g -> f = g.
-Proof. intros; apply extF; intro; apply fun_ext; easy. Qed.
+Proof. intros H; apply extF; intro; apply fun_ext, H. Qed.
 
 End FF_Facts0b.
 
@@ -284,17 +315,20 @@ Definition tripleF (x0 x1 x2 : E) : 'E^3 :=
     | inright _ => x2
     end.
 
+Definition eqF {n} (A : 'E^n) x i : Prop := A i = x.
+Definition neqF {n} (A : 'E^n) x i : Prop := A i <> x.
+
+(* Could be PEF (eqF A x). *)
 Definition inF {n} x (A : 'E^n) : Prop := exists i, x = A i.
 
+(* Could be PAF (fun i => PE (A i)). *)
 Definition inclF {n} (A : 'E^n) (PE : E -> Prop) : Prop := forall i, PE (A i).
 
 Definition invalF {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2) : Prop :=
   inclF A1 (inF^~ A2).
 
-Definition eqF {n} (A : 'E^n) x i : Prop := A i = x.
-Definition neqF {n} (A : 'E^n) x i : Prop := A i <> x.
-
-Definition equivF {n} (P Q : 'Prop^n) := forall i, P i <-> Q i.
+(* Could be PAF (equivF P Q). *)
+Definition equivFA {n} (P Q : 'Prop^n) := forall i, P i <-> Q i.
 
 Definition eqPF {n} (P : 'Prop^n) (A B : 'E^n) : Prop :=
   forall i, P i -> A i = B i.
@@ -1126,21 +1160,21 @@ Lemma invalF_P :
     invalF A1 A2 -> (forall i2, P (A2 i2)) -> forall i1, P (A1 i1).
 Proof. move=>> /invalF_fun [f Hf] H2 i1; rewrite Hf; easy. Qed.
 
-(** Properties of predicates equivF. *)
+(** Properties of predicates equivFA. *)
 
-Lemma equivF_refl : forall {n} (P : 'Prop^n), equivF P P.
+Lemma equivFA_refl : forall {n} (P : 'Prop^n), equivFA P P.
 Proof. easy. Qed.
 
-Lemma equivF_sym : forall {n} {P Q : 'Prop^n}, equivF P Q -> equivF Q P.
+Lemma equivFA_sym : forall {n} {P Q : 'Prop^n}, equivFA P Q -> equivFA Q P.
 Proof. easy. Qed.
 
-Lemma equivF_trans :
-  forall {n} (Q P R : 'Prop^n), equivF P Q -> equivF Q R -> equivF P R.
+Lemma equivFA_trans :
+  forall {n} (Q P R : 'Prop^n), equivFA P Q -> equivFA Q R -> equivFA P R.
 Proof. move=>> HPQ HQR i; rewrite HPQ; auto. Qed.
 
-Lemma equivF_eq_sym :
+Lemma equivFA_eq_sym :
   forall {n1 n2} (H : n1 = n2) {P1 : 'Prop^n1} {P2 : 'Prop^n2},
-    equivF P1 (castF (eq_sym H) P2) -> forall i1, P1 i1 <-> P2 (cast_ord H i1).
+    equivFA P1 (castF (eq_sym H) P2) -> forall i1, P1 i1 <-> P2 (cast_ord H i1).
 Proof. move=>>; rewrite castF_eq_sym; easy. Qed.
 
 (** Properties of predicates eqPF/neqPF. *)
@@ -1360,6 +1394,24 @@ intros n1 n2 H A2;  exists (fun i1 => A2 (cast_ord H i1)).
 apply extF; intro; unfold castF; f_equal; rewrite cast_ordKV; easy.
 Qed.
 
+Lemma sortedF_castF :
+  forall {leE : E -> E -> Prop} {n1 n2} (H : n1 = n2) {A : 'E^n1},
+    sortedF leE A -> sortedF leE (castF H A).
+Proof. move=>> HA i2 j2 H2; apply HA; easy. Qed.
+
+Lemma sortedF_castF_rev :
+  forall {leE : E -> E -> Prop} {n1 n2} (H : n1 = n2) {A : 'E^n1},
+    sortedF leE (castF H A) -> sortedF leE A.
+Proof.
+intros leE n1 n2 H A HA i1 j1 H1;
+    rewrite -(cast_ordK H i1) -(cast_ordK H j1); apply HA; easy.
+Qed.
+
+Lemma sortedF_castF_equiv :
+  forall {leE : E -> E -> Prop} {n1 n2} (H : n1 = n2) {A : 'E^n1},
+    sortedF leE A <-> sortedF leE (castF H A).
+Proof. intros; split; [apply sortedF_castF | apply sortedF_castF_rev]. Qed.
+
 Lemma invalF_castF_l_equiv :
   forall {m1 m2 n} (Hm : m1 = m2) (Am : 'E^m1) (An : 'E^n),
     invalF (castF Hm Am) An <-> invalF Am An.
@@ -1513,6 +1565,7 @@ assert (Hlf'b : lf' = map (f \o p1) (ord_enum n1.+1)).
 (* *)
 exists p1; split; [apply injF_bij; easy | apply incrF_equiv].
 intros i1 Hj1; rewrite !comp_correct; pose (j1 := Ordinal Hj1); fold j1.
+apply /ltP.
 assert (H : i1 < j1) by easy.
 destruct (proj1 ltn_equiv H) as [H1 H2].
 apply leq_neq_ltn;
@@ -1764,6 +1817,20 @@ Section WidenF_S_liftF_S_Facts1.
 
 Context {E : Type}.
 
+Lemma PAF_ind_l :
+  forall {n} {P : 'Prop^n.+1}, P ord0 -> PAF (liftF_S P) -> PAF P.
+Proof.
+intros n P H0 H1 i; destruct (ord_eq_dec i ord0) as [-> | Hi]; [easy |].
+rewrite -(lift_lower_S Hi); apply H1.
+Qed.
+
+Lemma PAF_ind_r :
+  forall {n} {P : 'Prop^n.+1}, PAF (widenF_S P) -> P ord_max -> PAF P.
+Proof.
+intros n P H0 H1 i; destruct (ord_eq_dec i ord_max) as [-> | Hi]; [easy |].
+rewrite -(widen_narrow_S Hi); apply H0.
+Qed.
+
 Lemma widenF_S_invalF :
   forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2),
     invalF A1 A2 -> invalF (widenF_S A1) A2.
@@ -2638,7 +2705,7 @@ Lemma insertF_inj_r :
   forall {n} (A B : 'E^n) x0 y0 i0,
     insertF A x0 i0 = insertF B y0 i0 -> x0 = y0.
 Proof.
-move=> n A B x0 y0 i0 /extF_rev H; specialize (H i0).
+move=> n A B x0 y0 i0 /extF_rev H; specialize (H i0); simpl in H.
 rewrite -> 2!insertF_correct_l in H; easy.
 Qed.
 
@@ -3018,6 +3085,13 @@ Proof.
 intros; split. intros; apply skipF_nextF_compat; easy. apply skipF_nextF_reg.
 Qed.
 
+Lemma PAF_ind_skipF :
+  forall {n} {P : 'Prop^n.+1} {i0}, P i0 -> PAF (skipF P i0) -> PAF P.
+Proof.
+intros n P i0 H0 H1 i; destruct (ord_eq_dec i i0) as [-> | Hi]; [easy |].
+rewrite -(skip_insert_ord Hi); apply H1.
+Qed.
+
 Lemma extF_skipF :
   forall {n} (A B : 'E^n.+1) i0,
     A i0 = B i0 -> skipF A i0 = skipF B i0 -> A = B.
@@ -3059,14 +3133,14 @@ Proof.
 move=>> HA1 Hi; split; [apply skipF_invalF_rev | apply skipF_invalF]; easy.
 Qed.
 
-Lemma skipF_coupleF_0 :
+Lemma skipF_2l :
   forall (A : 'E^2), skipF A ord0 = singleF (A ord_max).
 Proof.
 intros; apply extF; intro; rewrite ord1 singleF_0 skipF_correct_r; try easy.
 rewrite liftF_S_0 ord2_1_max; easy.
 Qed.
 
-Lemma skipF_coupleF_1 :
+Lemma skipF_2r :
   forall (A : 'E^2), skipF A ord_max = singleF (A ord0).
 Proof.
 intros; apply extF; intro;
@@ -3074,7 +3148,7 @@ intros; apply extF; intro;
 apply widenF_S_0.
 Qed.
 
-Lemma skipF_tripleF_0 :
+Lemma skipF_3l :
   forall (A : 'E^3), skipF A ord0 = coupleF (A ord_1) (A ord_max).
 Proof.
 intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
@@ -3082,7 +3156,7 @@ rewrite coupleF_0 skipF_correct_r; [apply liftF_S_0 | easy].
 rewrite coupleF_1 skipF_correct_r; [apply liftF_S_max | easy].
 Qed.
 
-Lemma skipF_tripleF_1 :
+Lemma skipF_3m :
   forall (A : 'E^3), skipF A ord_1 = coupleF (A ord0) (A ord_max).
 Proof.
 intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
@@ -3090,7 +3164,7 @@ rewrite coupleF_0 skipF_correct_l; [apply widenF_S_0 | now apply /ltP].
 rewrite coupleF_1 skipF_correct_r; [apply liftF_S_max | now apply /ltP].
 Qed.
 
-Lemma skipF_tripleF_2 :
+Lemma skipF_3r :
   forall (A : 'E^3), skipF A ord_max = coupleF (A ord0) (A ord_1).
 Proof.
 intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
@@ -3319,7 +3393,7 @@ Lemma skip2F_tripleF_01 :
 Proof.
 intros; apply extF; intro;
     rewrite ord1 singleF_0 skip2F_correct skipF_correct_r.
-rewrite liftF_S_0 skipF_tripleF_0 ord2_1_max coupleF_1; easy.
+rewrite liftF_S_0 skipF_3l ord2_1_max coupleF_1; easy.
 rewrite (insert_ord_correct_r _ ord_lt_0_1); easy.
 Qed.
 
@@ -3328,7 +3402,7 @@ Lemma skip2F_tripleF_02 :
 Proof.
 intros; apply extF; intro;
     rewrite ord1 singleF_0 skip2F_correct skipF_correct_l.
-rewrite widenF_S_0 skipF_tripleF_0 coupleF_0; easy.
+rewrite widenF_S_0 skipF_3l coupleF_0; easy.
 rewrite (insert_ord_correct_r _ ord_lt_0_max) lower_S_correct;
     apply ord_lt_0_pred_max.
 Qed.
@@ -3338,11 +3412,20 @@ Lemma skip2F_tripleF_12 :
 Proof.
 intros; apply extF; intro;
     rewrite ord1 singleF_0 skip2F_correct skipF_correct_l.
-rewrite widenF_S_0 skipF_tripleF_1 coupleF_0; easy.
+rewrite widenF_S_0 skipF_3m coupleF_0; easy.
 rewrite (insert_ord_correct_r _ ord_lt_1_max) lower_S_correct;
     apply ord_lt_0_pred_max.
 Qed.
 
+Lemma PAF_ind_skip2F :
+  forall {n} {P : 'Prop^n.+2} {i0 i1} (H : i1 <> i0),
+    P i0 -> P i1 -> PAF (skip2F P H) -> PAF P.
+Proof.
+intros n P i0 i1 Hi H0 H1 H2; rewrite skip2F_correct in H2.
+rewrite -(skip_insert_ord Hi) in H1.
+apply: (PAF_ind_skipF H0) (PAF_ind_skipF H1 H2).
+Qed.
+
 Lemma extF_skip2F :
   forall {n} (A B : 'E^n.+2) {i0 i1} (H : i1 <> i0),
     A i0 = B i0 -> A i1 = B i1 -> skip2F A H = skip2F B H -> A = B.
@@ -3409,7 +3492,7 @@ destruct (ord_eq_dec i i0) as [H0 | H0].
 (* i = i0 *)
 rewrite replaceF_correct_l H0; try easy.
 assert (Ha : (widen_S i0 < lift_S i0)%coq_nat).
-  rewrite widen_S_correct lift_S_correct; apply Nat.lt_succ_diag_r.
+  rewrite widen_S_correct lift_S_correct; apply nat_ltS.
 assert (Hb : widen_S i0 <> lift_S i0) by apply ord_lt_neq, Ha.
 replace i0 with (insert_ord Hb) at 3.
 rewrite skipF_correct insertF_correct_l; try easy.
@@ -3450,7 +3533,7 @@ Lemma replaceF_reg_l :
   forall {n} (A B : 'E^n) x0 y0 i0,
     replaceF A x0 i0 = replaceF B y0 i0 -> eqxF A B i0.
 Proof.
-move=>> /extF_rev H i Hi; specialize (H i).
+move=>> /extF_rev H i Hi; specialize (H i); simpl in H.
 erewrite 2!replaceF_correct_r in H; easy.
 Qed.
 
@@ -3458,7 +3541,7 @@ Lemma replaceF_reg_r :
   forall {n} (A B : 'E^n) x0 y0 i0,
     replaceF A x0 i0 = replaceF B y0 i0 -> x0 = y0.
 Proof.
-move=> n A B x0 y0 i0 /extF_rev H; specialize (H i0).
+move=> n A B x0 y0 i0 /extF_rev H; specialize (H i0); simpl in H.
 erewrite 2!replaceF_correct_l in H; easy.
 Qed.
 
@@ -3568,6 +3651,13 @@ rewrite -> replaceF_correct_r, 2!tripleF_1; easy.
 rewrite -> tripleF_2, replaceF_correct_l; easy.
 Qed.
 
+Lemma PAF_ind_replaceF :
+  forall {n} {P : 'Prop^n} {i0} p0, P i0 -> PAF (replaceF P p0 i0) -> PAF P.
+Proof.
+intros n P i0 p0 H0 H1 i; destruct (ord_eq_dec i i0) as [-> | Hi]; [easy |].
+rewrite -(replaceF_correct_r _ p0 Hi); easy.
+Qed.
+
 Lemma extF_replaceF :
   forall {n} (A B : 'E^n) x0 i0,
     A i0 = B i0 -> replaceF A x0 i0 = replaceF B x0 i0 -> A = B.
@@ -3688,6 +3778,16 @@ Proof.
 intros; unfold replace2F; rewrite replaceF_tripleF_1 replaceF_tripleF_2; easy.
 Qed.
 
+Lemma PAF_ind_replace2F :
+  forall {n} {P : 'Prop^n} {i0 i1} p0 p1,
+    P i0 -> P i1 -> PAF (replace2F P p0 p1 i0 i1) -> PAF P.
+Proof.
+intros n P i0 i1 p0 p1 H0 H1 H2; destruct (ord_eq_dec i1 i0) as [Hi | Hi].
+rewrite replace2F_correct_eq// in H2; apply (PAF_ind_replaceF p1 H1 H2).
+rewrite -(replaceF_correct_r _ p0 Hi) in H1.
+apply: (PAF_ind_replaceF p0 H0) (PAF_ind_replaceF _ H1 H2).
+Qed.
+
 Lemma extF_replace2F :
   forall {n} (A B : 'E^n) x0 x1 i0 i1,
     A i0 = B i0 -> A i1 = B i1 ->
@@ -4158,20 +4258,20 @@ Qed.
 
 Lemma filterPF_ext_l_gen :
   forall {n1 n2} (Hn : n1 = n2) {P1 : 'Prop^n1} {P2 : 'Prop^n2}
-      (HP : equivF P1 (castF (eq_sym Hn) P2)) (A1 : 'E^n1),
+      (HP : equivFA P1 (castF (eq_sym Hn) P2)) (A1 : 'E^n1),
     let A2 := castF Hn A1 in
     filterPF P1 A1 =
-      castF (eq_sym (lenPF_ext_gen Hn (equivF_eq_sym Hn HP))) (filterPF P2 A2).
+      castF (eq_sym (lenPF_ext_gen Hn (equivFA_eq_sym Hn HP))) (filterPF P2 A2).
 Proof.
 intros n1 n2 Hn P1 P2 HP A1 A2; unfold A2; subst; rewrite castF_refl; clear A2.
 apply extF; intro; unfold filterPF, castF; f_equal; apply ord_inj; simpl.
-assert (HP' : equivF P1 P2) by now intro; rewrite HP castF_eq_sym_refl.
+assert (HP' : equivFA P1 P2) by now intro; rewrite HP castF_eq_sym_refl.
 rewrite eq_sym_involutive (filterP_ord_ext HP')
-    (filterP_cast_ord_eq (lenPF_ext _) (lenPF_ext_gen _ (equivF_eq_sym _ _))); easy.
+    (filterP_cast_ord_eq (lenPF_ext _) (lenPF_ext_gen _ (equivFA_eq_sym _ _))); easy.
 Qed.
 
 Lemma filterPF_ext_l :
-  forall {n P Q} (H : equivF P Q) (A : 'E^n),
+  forall {n P Q} (H : equivFA P Q) (A : 'E^n),
     filterPF P A = castF (eq_sym (lenPF_ext H)) (filterPF Q A).
 Proof.
 intros; apply extF; intro; unfold filterPF, castF; f_equal.
@@ -4197,7 +4297,7 @@ Lemma filterPF_castF_l :
       castF (eq_sym (lenPF_castF H P1)) (filterPF P1 (castF (eq_sym H) A2)).
 Proof.
 intros n1 n2 H P1 A2; subst.
-assert (HP : equivF (castF (erefl n2) P1) P1) by now rewrite castF_refl.
+assert (HP : equivFA (castF (erefl n2) P1) P1) by now rewrite castF_refl.
 rewrite (filterPF_ext_l HP) eq_sym_refl (castF_refl A2); f_equal; easy.
 Qed.
 
@@ -4208,7 +4308,7 @@ Lemma filterPF_castF_r :
             (filterPF (castF (eq_sym H) P2) A1).
 Proof.
 intros n1 n2 H P2 A1; subst; rewrite eq_sym_refl castF_refl.
-assert (HP : equivF (castF (erefl n2) P2) P2) by now rewrite castF_refl.
+assert (HP : equivFA (castF (erefl n2) P2) P2) by now rewrite castF_refl.
 rewrite (filterPF_ext_l HP) castF_comp castF_refl; easy.
 Qed.
 
@@ -4248,7 +4348,7 @@ Lemma filterPF_ind_l_in :
         (concatF (singleF (A ord0)) (filterPF (liftF_S P) (liftF_S A))).
 Proof.
 intros n P HP0 A; apply (castF_inj (lenPF_ind_l_in HP0)); rewrite castF_id.
-assert (HP1 : equivF P (castF_1pS (concatF (singleF (P ord0)) (liftF_S P))))
+assert (HP1 : equivFA P (castF_1pS (concatF (singleF (P ord0)) (liftF_S P))))
     by now rewrite -concatF_splitF_S1p.
 rewrite (filterPF_ext_l HP1) {1}(concatF_splitF_S1p A) filterPF_castF !castF_comp.
 pose (P0 := singleF (P ord0)); fold P0; pose (P' := liftF_S P); fold P'.
@@ -4275,7 +4375,7 @@ assert (H0 : cast_ord (lenPF_ind_l_in HP0) (cast_ord (eq_sym H) j) <> ord0).
   rewrite cast_ord_comp; contradict Hj2; apply cast_ord_0 in Hj2.
   rewrite Hj2; apply Nat.lt_0_1.
 rewrite filterP_ord_ind_l_in_n0 lift_S_correct -add1n; f_equal.
-assert (HP2 : equivF (liftF_S (concatF P0 P')) (liftF_S P)).
+assert (HP2 : equivFA (liftF_S (concatF P0 P')) (liftF_S P)).
   unfold P0, P'; rewrite concatF_splitF_S1p'.
   unfold castF_S1p; rewrite castF_refl; easy.
 rewrite (filterP_ord_ext HP2).
@@ -4290,7 +4390,7 @@ Lemma filterPF_ind_l_out :
       castF (eq_sym (lenPF_ind_l_out HP)) (filterPF (liftF_S P) (liftF_S A)).
 Proof.
 intros n P HP A; apply (castF_inj (lenPF_ind_l_out HP)); rewrite castF_id.
-assert (HP1 : equivF P (castF_1pS (concatF (singleF (P ord0)) (liftF_S P))))
+assert (HP1 : equivFA P (castF_1pS (concatF (singleF (P ord0)) (liftF_S P))))
     by now rewrite -concatF_splitF_S1p.
 rewrite (filterPF_ext_l HP1) {1}(concatF_splitF_S1p A) filterPF_castF !castF_comp.
 pose (P0 := singleF (P ord0)); fold P0; pose (P' := liftF_S P); fold P'.
@@ -4306,7 +4406,7 @@ apply lift_S_not_first.
 (* *)
 rewrite concatF_correct_r; f_equal; apply ord_inj; simpl; apply addn_is_subn.
 rewrite filterP_ord_ind_l_out lift_S_correct -add1n; f_equal.
-assert (HP2 : equivF (liftF_S (concatF P0 P')) (liftF_S P)).
+assert (HP2 : equivFA (liftF_S (concatF P0 P')) (liftF_S P)).
   unfold P0, P'; rewrite concatF_splitF_S1p'.
   unfold castF_S1p; rewrite castF_refl; easy.
 rewrite (filterP_ord_ext HP2) !cast_ord_comp cast_ord_id; easy.
@@ -4344,7 +4444,7 @@ Lemma filterPF_ind_r_in :
         (concatF (filterPF (widenF_S P) (widenF_S A)) (singleF (A ord_max))).
 Proof.
 intros n P HPn A; apply (castF_inj (lenPF_ind_r_in HPn)); rewrite castF_id.
-assert (HP1 : equivF P (castF_p1S (concatF (widenF_S P) (singleF (P ord_max)))))
+assert (HP1 : equivFA P (castF_p1S (concatF (widenF_S P) (singleF (P ord_max)))))
     by now rewrite -concatF_splitF_Sp1.
 rewrite (filterPF_ext_l HP1) {1}(concatF_splitF_Sp1 A) filterPF_castF !castF_comp.
 pose (P' := widenF_S P); fold P'; pose (Pn := singleF (P ord_max)); fold Pn.
@@ -4397,7 +4497,7 @@ Lemma filterPF_ind_r_out :
       castF (eq_sym (lenPF_ind_r_out HP)) (filterPF (widenF_S P) (widenF_S A)).
 Proof.
 intros n P HPn A; apply (castF_inj (lenPF_ind_r_out HPn)); rewrite castF_id.
-assert (HP1 : equivF P (castF_p1S (concatF (widenF_S P) (singleF (P ord_max)))))
+assert (HP1 : equivFA P (castF_p1S (concatF (widenF_S P) (singleF (P ord_max)))))
     by now rewrite -concatF_splitF_Sp1.
 rewrite (filterPF_ext_l HP1) {1}(concatF_splitF_Sp1 A) filterPF_castF !castF_comp.
 pose (P' := widenF_S P); fold P'; pose (Pn := singleF (P ord_max)); fold Pn.
@@ -4465,7 +4565,7 @@ Lemma filterPF_concatF :
 Proof.
 intros n1 n2; induction n2 as [|n2 IHn2]; intros P1 P2 A1 A2.
 (* *)
-assert (HP : equivF (concatF P1 P2) (castF (addn0_sym n1) P1))
+assert (HP : equivFA (concatF P1 P2) (castF (addn0_sym n1) P1))
     by now rewrite concatF_nil_r.
 rewrite (filterPF_ext_l HP) (concatF_nil_r A1) filterPF_castF
     (concatF_nil_r' (lenPF_nil P2) (filterPF _ _)).
@@ -4473,10 +4573,10 @@ rewrite !castF_comp; apply castF_eq_l.
 (* *)
 apply (castF_inj (eq_sym (lenPF_castF (addnS n1 n2) (concatF P1 P2)))).
 rewrite -filterPF_castF filterPF_ind_r (filterPF_ind_r P2) castF_comp.
-assert (HP : equivF (widenF_S (castF (addnS n1 n2) (concatF P1 P2)))
+assert (HP : equivFA (widenF_S (castF (addnS n1 n2) (concatF P1 P2)))
     (concatF P1 (widenF_S P2))) by now rewrite widenF_S_concatF.
 rewrite (filterPF_ext_l HP) (widenF_S_concatF A1 A2) IHn2.
-assert (HPmax : equivF (singleF (castF (addnS n1 n2) (concatF P1 P2) ord_max))
+assert (HPmax : equivFA (singleF (castF (addnS n1 n2) (concatF P1 P2) ord_max))
     (singleF (P2 ord_max))) by now rewrite concatF_last.
 rewrite (filterPF_ext_l HPmax) (concatF_last A1 A2).
 (* To help human beings...
@@ -4500,7 +4600,7 @@ Lemma filterPF_splitF :
                      (filterPF (lastF P) (lastF A))).
 Proof.
 intros n1 n2 P A.
-assert (HP : equivF P (concatF (firstF P) (lastF P)))
+assert (HP : equivFA P (concatF (firstF P) (lastF P)))
     by now rewrite -concatF_splitF.
 rewrite (filterPF_ext_l HP) {1}(concatF_splitF A) filterPF_concatF.
 rewrite !castF_comp; apply castF_eq_l.
@@ -4753,69 +4853,49 @@ rewrite (filterP_ord_Rg_aux2 Hf HP).
 apply filterP_ord_Rg_aux3.
 Qed.
 
-(* TODO FC (31/01/2024): this should be generalizable to any predicate on f and i2. *)
-Lemma Rg_0_liftF_S : forall  {n1 n2} {f : 'I_{n1.+1,n2}},
-   Rg f = union (fun t => t = f ord0) (Rg (liftF_S f)).
+(* TODO FC (01/02/2024): try using PAF_ind_l. *)
+Lemma Rg_0_liftF_S :
+  forall  {n1 n2} {f : 'I_{n1.+1,n2}},
+    Rg f = union (eq^~ (f ord0)) (Rg (liftF_S f)).
 Proof.
-intros n1 n2 f; unfold Rg.
-replace fullset with (union (fun t:'I_n1.+1 => t = ord0) (fun t:'I_n1.+1 => t <> ord0)).
-rewrite image_union; f_equal.
-apply subset_ext_equiv; split; intros x Hx.
-inversion Hx; subst; easy.
-rewrite Hx; easy.
-apply subset_ext_equiv; split; intros x Hx.
-inversion Hx as (i,Hi1,Hi2); rewrite image_eq.
-exists (lower_S Hi1); split; try easy; unfold liftF_S; f_equal.
-rewrite lift_lower_S; easy.
-inversion Hx as (i,Hi1,Hi2); rewrite image_eq.
-exists (lift_S i); split; try easy.
-unfold union; apply extF; intros i; unfold fullset; simpl.
-apply boolp.propT; case (ord_eq_dec i ord0);[left|right]; easy.
+intros n1 n2 f; apply subset_ext_equiv; split.
+(* *)
+intros i2 [i1 _]; destruct (ord_eq_dec i1 ord0) as [-> | Hi1]; [left; easy |].
+right; rewrite -(lift_lower_S Hi1); fold (liftF_S f (lower_S Hi1)); easy.
+(* *)
+intros i2 [-> | [i1 _]]; easy.
 Qed.
 
-Lemma incrF_Rg_eq_eq_aux: forall {n1 n2} {f g : 'I_{n1.+1,n2}}, 
-     incrF f -> incrF g -> Rg f = Rg g -> (f ord0 <= g ord0)%coq_nat.
+Lemma incrF_Rg_le_0 :
+  forall {n1 n2} {f g : 'I_{n1.+1,n2}},
+    incrF f -> incrF g -> Rg f = Rg g -> (f ord0 <= g ord0)%coq_nat.
 Proof.
 intros n1 n2 f g Hf Hg H.
 case (Nat.le_gt_cases (f ord0) (g ord0)); try easy; intros H1.
 assert (H2: Rg g (g ord0)) by easy.
 rewrite -H in H2; inversion H2 as (t,_,Ht2).
 rewrite -Ht2 in H1; contradict H1; apply Nat.le_ngt.
-case (ord_eq_dec ord0 t); intros Ht.
+case (ord_eq_dec t ord0); intros Ht.
 rewrite Ht; auto with arith.
-apply /leP; apply ltnW; apply Hf; simpl.
-apply /ltP; destruct t as (t,Htt); simpl.
-case_eq t; simpl; auto with arith.
-intros Ht3; contradict Ht.
-apply ord_inj; simpl; easy.
+apply Nat.lt_le_incl, Hf; simpl.
+apply Nat.neq_0_lt_0, (ord_neq_compat Ht).
 Qed.
 
-Lemma incrF_Rg_eq_eq : forall {n1 n2} {f g : 'I_{n1,n2}}, 
-     incrF f -> incrF g -> Rg f = Rg g -> f = g.
-Proof.
-intros n1; induction n1.
-intros n2 f g Hf Hg H; apply extF; intros i.
-destruct i; easy.
-intros n2 f g Hf Hg H.
-assert (Y1: f ord0 = g ord0).
-apply ord_inj; apply Nat.le_antisymm.
-apply incrF_Rg_eq_eq_aux; easy.
-apply incrF_Rg_eq_eq_aux; easy.
-apply extF_liftF_S; [easy |].
-apply IHn1.
-intros i j Hij; apply Hf; easy.
-intros i j Hij; apply Hg; easy.
-unfold Rg; apply union_inj_r with (fun t => t = f ord0).
-intros i Hi; rewrite Hi; intros H1.
-inversion H1 as (j,Hj1,Hj2); unfold liftF_S in Hj2.
-apply incrF_inj in Hf; apply Hf in Hj2; easy.
-intros i Hi; rewrite Hi; intros H1.
-inversion H1 as (j,Hj1,Hj2); unfold liftF_S in Hj2.
-apply incrF_inj in Hg; rewrite Y1 in Hj2.
-apply Hg in Hj2; easy.
-apply trans_eq with (Rg f);[|rewrite H].
-apply sym_eq, Rg_0_liftF_S.
-rewrite Rg_0_liftF_S; f_equal; rewrite Y1; easy.
+Lemma ext_fun_incrF_Rg :
+  forall {n1 n2} {f g : 'I_{n1,n2}},
+    incrF f -> incrF g -> Rg f = Rg g -> f = g.
+Proof.
+intros n1; induction n1; [intros; apply extF; intros [i Hi]; easy |].
+intros n2 f g Hf Hg HRg.
+assert (H0 : f ord0 = g ord0)
+    by now apply ord_inj, Nat.le_antisymm; apply incrF_Rg_le_0.
+apply extF_liftF_S; [easy | apply IHn1].
+move=>> /ltP H; apply Hf; apply /ltP; easy.
+move=>> /ltP H; apply Hg; apply /ltP; easy.
+apply union_inj_r with (eq^~ (f ord0)); [| rewrite H0 |].
+move=> i2 -> H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hf) in Hi1; easy.
+move=> i2 -> H1; inversion H1 as [i1 _ Hi1]; apply (incrF_inj Hg) in Hi1; easy.
+apply trans_eq with (Rg f); [apply sym_eq | rewrite HRg H0]; apply Rg_0_liftF_S.
 Qed.
 
 Lemma filterP_ord_w_incrF :
@@ -4824,7 +4904,7 @@ Lemma filterP_ord_w_incrF :
     let H := lenPF_extendPF (incrF_inj Hf) HP in
     f \o filterP_ord = filterP_ord \o (cast_ord H).
 Proof.
-intros; apply incrF_Rg_eq_eq.
+intros; apply ext_fun_incrF_Rg.
 apply incrF_comp; [apply filterP_ord_incrF | easy].
 apply filterP_cast_ord_incrF.
 apply filterP_ord_Rg.
diff --git a/FEM/Algebra/Monoid_compl.v b/FEM/Algebra/Monoid_compl.v
index 1dd835e2a7720429a7a3ac5d9501e13dee1dd078..d9ce938449d104795aad27a2510a7930696e59d6 100644
--- a/FEM/Algebra/Monoid_compl.v
+++ b/FEM/Algebra/Monoid_compl.v
@@ -3158,159 +3158,34 @@ replace (widen_S (splitn_ord1 j))
 apply ord_inj; easy.
 Qed.
 
-Definition is_orderedF (Q : G -> G -> Prop) {n} (A : 'G^n) :=
-  forall (i j : 'I_n), (i < j)%coq_nat -> Q (A i) (A j).
-
-Lemma is_orderedF_nil : forall Q (A : 'G^0), is_orderedF Q A.
-Proof.
-intros Q a i j H.
-exfalso; apply I_0_is_empty; apply (inhabits i).
-Qed.
-
-Lemma is_orderedF_one : forall Q (A : 'G^1), is_orderedF Q A.
-Proof.
-intros Q a i j H; contradict H.
-rewrite 2!ord1; auto with zarith.
-Qed.
-
-Lemma is_orderedF_inj :
-  forall (Q : G -> G -> Prop) {n} (A : 'G^n),
-    (forall x y, Q x y -> x <> y) -> is_orderedF Q A -> injective A.
-Proof.
-intros Q n A HQ H.
-intros i j H1.
-case (Nat.le_gt_cases i j); intros H2.
-case (proj1 (Nat.lt_eq_cases i j) H2); intros H3.
-contradict H1; apply HQ; apply H; easy.
-apply ord_inj; easy.
-apply sym_eq in H1.
-contradict H1; apply HQ; apply H; easy.
-Qed.
-
-Lemma is_orderedF_castF :
-  forall Q {n m} (H : n=m) (A : 'G^n), is_orderedF Q A -> is_orderedF Q (castF H A).
-Proof.
-intros Q n m H A H1 i j H2.
-unfold castF; apply H1.
-simpl; auto.
-Qed.
-
-Lemma is_orderedF_S_aux : forall (Q: G -> G -> Prop) {n} (g:'G^n.+1),
-     (forall c d e, Q c d -> Q d e -> Q c e) ->
-     (forall m (i:'I_n.+1) (H: i+m+1 < n.+1 ), 
-           Q (g i)
-             (g (Ordinal H))) ->
-      is_orderedF Q g.
-Proof.
-intros Q n g Htrans Hi i j Hij.
-specialize (Hi (j-i-1)%coq_nat i).
-assert (H: (i + (j - i - 1)%coq_nat + 1 < n.+1)).
-apply /ltP; simpl; rewrite -plusE -minusE.
-apply Nat.le_lt_trans with j; auto with zarith arith.
-apply /ltP; destruct j; easy.
-specialize (Hi H).
-replace j with (Ordinal H); try easy.
-apply ord_inj; simpl.
-rewrite -plusE -minusE; auto with zarith arith.
-Qed.
-
-Lemma is_orderedF_S : forall (Q: G -> G -> Prop) {n} (g:'G^n.+1),
-     (forall c d e, Q c d -> Q d e -> Q c e) ->
-     (forall (i:'I_n.+1) (H: i <> ord_max ), 
-           Q (g i)
-             (g (lift_S (narrow_S H)))) ->
-      is_orderedF Q g.
-Proof.
-intros Q n g Htrans Hi.
-apply is_orderedF_S_aux; try easy.
-intros m; induction m.
-intros i K.
-assert (K': i <> ord_max).
-assert (H: (i+0+1 < n.+1)%coq_nat).
-apply /ltP; auto with arith.
-intros V; contradict H; rewrite V; simpl.
-rewrite -plusE; auto with zarith.
-specialize (Hi i K').
-replace (Ordinal K) with  (lift_S (narrow_S K')); try easy.
-apply ord_inj; simpl.
-rewrite bump_r; try rewrite -plusE; auto with arith zarith.
-intros i K.
-assert (K' : i <> ord_max).
-assert (H: (i+m.+1 +1 < n.+1)%coq_nat).
-apply /ltP; auto with arith.
-intros V; contradict H; rewrite V; simpl.
-rewrite -plusE; auto with zarith.
-pose (i' := (lift_S (narrow_S K'))).
-apply Htrans with (g i').
-apply Hi.
-assert (K'': i' + m + 1 < n.+1).
-apply /ltP; simpl.
-rewrite bump_r; auto with arith.
-assert (H: (i+m.+1 +1 < n.+1)%coq_nat).
-apply /ltP; auto with arith.
-repeat rewrite -plusE; repeat rewrite -plusE in H.
-auto with zarith.
-specialize (IHm i' K'').
-replace (Ordinal K) with (Ordinal K''); try easy.
-apply ord_inj; simpl.
-rewrite bump_r; repeat rewrite -plusE; auto with zarith.
-Qed.
-
-Lemma concatnF_order : forall (Q: G -> G -> Prop) {n} (b:'nat^n.+1)  
-     (g: forall (i:'I_n.+1), 'I_(b i).+1 -> G),
-     (forall c d e, Q c d -> Q d e -> Q c e) ->
-     (forall i, is_orderedF Q (g i)) ->
-
-    (forall (i:'I_n.+1) (H: i <> ord_max ), 
-           Q (g i ord_max)
-             (g (lift_S (narrow_S H)) ord0)) ->
-
-     is_orderedF Q (concatnF g).
+Lemma concatnF_order :
+  forall (Q: G -> G -> Prop) {n} (b:'nat^n.+1) (g: forall i, 'I_(b i).+1 -> G),
+    (forall c d e, Q c d -> Q d e -> Q c e) ->
+    (forall i, sortedF Q (g i)) ->
+    (forall (i : 'I_n.+1) (H: i <> ord_max ),
+      Q (g i ord_max) (g (lift_S (narrow_S H)) ord0)) ->
+    sortedF Q (concatnF g).
 Proof.
 intros Q n b g Htrans H1 H2.
-rewrite -(castF_refl (concatnF g)).
-rewrite -(eq_trans_sym_inv_r (sum_is_S b)).
-rewrite -castF_comp.
-apply is_orderedF_castF.
-apply is_orderedF_S; try easy.
+apply (sortedF_castF_equiv (sum_is_S b)), sortedF_equiv; [easy |].
 intros i Hi; unfold castF.
-pose (i':=cast_ord (eq_sym (sum_is_S b)) i).
-pose (j':=(cast_ord (eq_sym (sum_is_S b)) (lift_S (narrow_S Hi)))).
+pose (i' := cast_ord (sym_eq (sum_is_S b)) i).
+pose (j' := cast_ord (sym_eq (sum_is_S b)) (Ordinal Hi)).
 assert (Q (concatnF g i') (concatnF g j')); try easy.
-case (splitn_ord1_S i' j').
-unfold j' ; unfold i'; simpl; rewrite bump_r; auto with arith.
+destruct (splitn_ord1_S i' j') as [[K1 K2] | [K1 [K2 K3]]]; [easy |..].
 (* *)
-intros (K1,K2).
-rewrite (splitn_ord i').
-rewrite (splitn_ord j').
-rewrite 2!concatn_ord_correct.
-assert (T: forall i1 i2 j1 j2, 
-   nat_of_ord i1 = nat_of_ord i2 -> (nat_of_ord j1 < nat_of_ord j2)%coq_nat 
-      -> Q (g i1 j1) (g i2 j2)).
-intros i1 i2 j1 j2 H H'.
-assert (M1 : i1 = i2).
-apply ord_inj; easy.
-subst.
-apply H1; easy.
-apply T; clear T.
-rewrite K1; easy.
-rewrite K2; auto with arith.
+rewrite (splitn_ord i') (splitn_ord j') !concatn_ord_correct.
+assert (HQ : forall i1 i2 (j1 : 'I_(b i1).+1) (j2 : 'I_(b i2).+1),
+    i1 = i2 -> (j1 < j2)%coq_nat -> Q (g i1 j1) (g i2 j2))
+    by now intros; subst; apply H1.
+apply HQ; [easy | rewrite K2; apply nat_ltS].
 (* *)
-intros (K1,(K2,K3)).
-rewrite (splitn_ord i').
-rewrite (splitn_ord j').
-rewrite 2!concatn_ord_correct.
-rewrite K2 K3.
-pose (l:=(splitn_ord1 i')).
-assert (Hl: l <> ord_max).
-intros V.
-absurd (splitn_ord1 j' < n.+1)%coq_nat.
-2: apply /ltP; easy.
-apply Arith_prebase.le_not_lt_stt.
-rewrite K1; fold l; rewrite V; simpl; auto with arith.
-replace (splitn_ord1 j') with (lift_S (narrow_S Hl)).
-apply H2.
-apply ord_inj; easy.
+assert (K4 : splitn_ord1 i' <> ord_max)
+    by now intros H; absurd (splitn_ord1 j' < n.+1)%coq_nat;
+      [apply Nat.nlt_ge; rewrite K1 H | apply /ltP].
+rewrite (splitn_ord i') (splitn_ord j') !concatn_ord_correct K2 K3.
+replace (splitn_ord1 j') with (lift_S (narrow_S K4));
+    [apply H2 | apply ord_inj; easy].
 Qed.
 
 End ConcatnF_Facts.
diff --git a/FEM/Algebra/nat_compl.v b/FEM/Algebra/nat_compl.v
index c7421fabee6c823c0eb531e952c5742124c87479..35935264430a5e8c0ff72cb8f889bd0938ff92bd 100644
--- a/FEM/Algebra/nat_compl.v
+++ b/FEM/Algebra/nat_compl.v
@@ -147,47 +147,27 @@ apply HP; move=> m1 n1 /Nat.le_lteq Hm1 /Nat.le_lteq Hn1 H1.
 destruct Hm1; subst; try now apply Hm.
 destruct Hn1; subst; try now apply Hn.
 lia.
-(* Proof using chatGPT.
-intros P HP; cut (forall s m n, m + n <= s -> P m n).
-- intros H m n; apply (H (m + n)); easy.
-- induction s as [| s IHs].
-  + move=>>; rewrite -plusE; move=> /leP /Nat.le_0_r /Nat.eq_add_0 [Hm Hn]; subst.
-    apply HP; move=>> /Nat.le_0_r -> /Nat.le_0_r ->; easy.
-  + move=>> /leP /Nat.le_lteq [H | H]; apply HP; move=>> Hm1 Hn1 H1.
-    * apply IHs; apply /leP; lia.
-    * apply Nat.le_lteq in Hm1, Hn1.
-      destruct Hm1, Hn1; subst; try lia; apply IHs; apply /leP; lia.
-*)
 Qed.
 
-Lemma lt_2_dec : forall {n}, n < 2 -> {n = 0} + {n = 1}.
-Proof.
-intros n H; induction n as [| n Hn].
-left; easy.
-destruct Hn as [Hn | Hn]; try auto with arith.
-contradict H; rewrite Hn; easy.
-Qed.
+Lemma nat_le_total : forall m n, (m <= n)%coq_nat \/ (n <= m)%coq_nat.
+Proof. intros; apply Nat.le_ge_cases. Qed.
 
-Lemma le_1_dec : forall {n}, n <= 1 -> {n = 0} + {n = 1}.
-Proof. intros; apply lt_2_dec; easy. Qed.
-
-Lemma lt_3_dec : forall {n}, n < 3 -> {n = 0} + {n = 1} + {n = 2}.
-Proof.
-intros n H; induction n as [| n Hn].
-left; left; easy.
-destruct Hn as [[Hn | Hn] | Hn]; try auto with arith.
-contradict H; rewrite Hn; easy.
-Qed.
-
-Lemma le_2_dec : forall {n}, n <= 2 -> {n = 0} + {n = 1} + {n = 2}.
-Proof. intros; apply lt_3_dec; easy. Qed.
+Lemma nat_lt_total_strict :
+  forall m n, m <> n -> (m < n)%coq_nat \/ (n < m)%coq_nat.
+Proof. move=>>; apply Nat.lt_gt_cases. Qed.
 
 Lemma nat_eq_le : forall m n, m = n -> (m <= n)%coq_nat.
 Proof. Lia.lia. Qed.
 
+Lemma le_neq_lt : forall m n, (m <= n)%coq_nat -> m <> n -> (m < n)%coq_nat.
+Proof. intros; apply Nat.le_neq; easy. Qed.
+
 Lemma nat_leS : forall n, (n <= n.+1)%coq_nat.
 Proof. exact Nat.le_succ_diag_r. Qed.
 
+Lemma nat_ltS : forall n, (n < n.+1)%coq_nat.
+Proof. exact Nat.lt_succ_diag_r. Qed.
+
 Lemma nat_le_ltS : forall {n i}, (i <= n)%coq_nat -> (i < n.+1)%coq_nat.
 Proof. Lia.lia. Qed.
 
@@ -311,6 +291,35 @@ Proof. move=>> /ltP; easy. Qed.
 Lemma le_leq : forall {m n}, (m <= n)%coq_nat -> m <= n.
 Proof. move=>> /leP; easy. Qed.
 
+(* TODO FC (01/02/2024): rename -> ltn_2_dec. *)
+Lemma lt_2_dec : forall {n}, n < 2 -> {n = 0} + {n = 1}.
+Proof.
+intros n H; induction n as [| n Hn].
+left; easy.
+destruct Hn as [Hn | Hn]; try auto with arith.
+contradict H; rewrite Hn; easy.
+Qed.
+
+(* TODO FC (01/02/2024): rename -> leq_1_dec. *)
+Lemma le_1_dec : forall {n}, n <= 1 -> {n = 0} + {n = 1}.
+Proof. intros; apply lt_2_dec; easy. Qed.
+
+(* TODO FC (01/02/2024): rename -> ltn_3_dec. *)
+Lemma lt_3_dec : forall {n}, n < 3 -> {n = 0} + {n = 1} + {n = 2}.
+Proof.
+intros n H; induction n as [| n Hn].
+left; left; easy.
+destruct Hn as [[Hn | Hn] | Hn]; try auto with arith.
+contradict H; rewrite Hn; easy.
+Qed.
+
+(* TODO FC (01/02/2024): rename -> leq_2_dec. *)
+Lemma le_2_dec : forall {n}, n <= 2 -> {n = 0} + {n = 1} + {n = 2}.
+Proof. intros; apply lt_3_dec; easy. Qed.
+
+Lemma ltnSS : forall {m n}, (m < n) = (m.+1 < n.+1).
+Proof. intros; rewrite ltnS; easy. Qed.
+
 Lemma ltnSSn : forall {n}, n < n.+2.
 Proof. easy. Qed.
 
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 99d96f0e2f00e703cfe65f293d2393cd6c1c33f5..76957c43455d8a33caf2d4fa7c4cc72964a3a288 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -5,7 +5,7 @@ Set Warnings "-notation-overridden".
 From mathcomp Require Import eqtype ssrnat seq path fintype bigop boolp.
 Set Warnings "notation-overridden".
 
-From Lebesgue Require Import nat_compl Subset Function.
+From Lebesgue Require Import logic_compl nat_compl Subset Function.
 
 From FEM Require Import Compl nat_compl.
 
@@ -122,17 +122,12 @@ Lemma injS_equiv_seq :
   forall {P : pred T} {sT : subType (T:=T) P} {f : T -> sT},
     injS P f <-> forall s, all P s -> { in s &, injective f }.
 Proof.
-intros P sT f; split.
-(* *)
-intros H s Hs x y Hx Hy; apply H.
-generalize Hx; apply /allP; easy.
-generalize Hy; apply /allP; easy.
-(* *)
+move=>>; split.
+intros H s Hs x y Hx Hy; apply H; [move: Hx | move: Hy]; apply /allP; easy.
 intros H x y Hx Hy; apply (H [:: x; y]).
-apply /all_filterP; simpl.
-rewrite Hx Hy; easy.
-rewrite in_cons eq_refl; easy.
-rewrite in_cons mem_seq1 eq_refl; apply orbT.
+simpl; rewrite Hx Hy; easy.
+rewrite !in_cons eq_refl; apply orTb.
+rewrite !in_cons eq_refl; apply orbT.
 Qed.
 
 End Seq_compl2.
@@ -751,67 +746,6 @@ Admitted.
 End Ord_compl3.
 
 
-Section Ord_compl4.
-
-(** Definition and properties of incrF/ord_leq. *)
-
-Definition incrF {n1 n2} (f : 'I_{n1,n2}) : Prop :=
-    forall (i1 j1 : 'I_n1), i1 < j1 -> f i1 < f j1.
-
-Definition incrF_S {n1 n2} (f : 'I_{n1,n2}) : Prop :=
-    forall (i1 : 'I_n1) (Hj1 : i1.+1 < n1), f i1 < f (Ordinal Hj1).
-
-Lemma incrF_equiv : forall {n1 n2} (f : 'I_{n1,n2}), incrF f <-> incrF_S f.
-Proof.
-intros n1 n2 f; split; intros Hf; [move=>>; apply Hf, ltnSn |].
-intros i1 k1 H1; pose (p := k1 - i1).
-assert (Hp : k1 = i1 + p :> nat) by now apply sym_eq, subnKC, ltnW.
-assert (Hj1 : i1 + p < n1) by admit. pose (j1 := Ordinal Hj1).
-assert (H : k1 = j1) by now apply ord_inj. rewrite H.
-
-(*
-move: j1 H1 p Hp.
-induction p as [|p]; [rewrite Hp -addn0_sym ltnn in H1; easy |].
-apply (ltn_trans _).
-*)
-
-
-
-
-
-Admitted.
-
-Lemma incrF_inj : forall {n1 n2} {f : 'I_{n1,n2}}, incrF f -> injective f.
-Proof.
-move=>> Hf i1 j1; apply contra_equiv;
-    move=> /ord_neq_compat /not_eq [/ltP H1 | /ltP H1]; [| apply not_eq_sym];
-    apply ord_neq, Nat.lt_neq; apply /ltP; apply Hf, H1.
-Qed.
-
-Lemma incrF_comp :
-  forall {n1 n2 n3} {f : 'I_{n1,n2}} {g : 'I_{n2,n3}},
-    incrF f -> incrF g -> incrF (g \o f).
-Proof. move=>> Hf Hg i1 j1 H1; apply Hg, Hf; easy. Qed.
-
-Definition ord_leq {n} : rel 'I_n := fun i j => i <= j.
-
-Lemma ord_leq_refl : forall {n} (i : 'I_n), ord_leq i i.
-Proof. intros; apply leqnn. Qed.
-
-Lemma ord_leq_antisym :
-  forall {n} (i j : 'I_n), ord_leq i j -> ord_leq j i -> i = j.
-Proof. intros; apply ord_inj, anti_leq; apply /andP; easy. Qed.
-
-Lemma ord_leq_trans :
-  forall {n} (i j k : 'I_n), ord_leq i j -> ord_leq j k -> ord_leq i k.
-Proof. move=>>; apply leq_trans. Qed.
-
-Lemma ord_leq_total : forall {n} (i j : 'I_n), ord_leq i j || ord_leq j i.
-Proof. intros; apply leq_total. Qed.
-
-End Ord_compl4.
-
-
 (** Specific ordinal transformations.
 
   Notations.
@@ -940,6 +874,172 @@ Proof. intros; apply not_eq_sym, widen_not_lift_S. Qed.
 End Widen_Lift_S.
 
 
+Section Ord_compl4a.
+
+(** Definition and properties of sortedF. *)
+
+Context {T : Type}.
+
+Variable leT : T -> T -> Prop.
+
+Definition sortedF {n} (A : 'I_n -> T) :=
+  forall (i j : 'I_n), (i < j)%coq_nat -> leT (A i) (A j).
+
+Definition sortedF_S {n} (A : 'I_n -> T) :=
+  forall (i : 'I_n) (Hi1 : i.+1 < n), leT (A i) (A (Ordinal Hi1)).
+
+Lemma sortedF_nil : forall (A : 'I_0 -> T), sortedF A.
+Proof. intros A i; destruct i; easy. Qed.
+
+Lemma sortedF_one : forall (A : 'I_1 -> T), sortedF A.
+Proof. move=>> H; contradict H; rewrite !ord1; apply Nat.lt_irrefl. Qed.
+
+(* leT is assumed irreflexive. *)
+Lemma sortedF_inj :
+  forall {n} {A : 'I_n -> T}, (forall x, ~ leT x x) -> sortedF A -> injective A.
+Proof.
+intros n A HT HA i j H1.
+assert (HT' : forall x y, leT x y -> x <> y)
+    by now move=>>; rewrite contra_not_r_equiv; intro; subst.
+destruct (lt_eq_lt_dec i j) as [[H2 | H2] | H2]; [..| apply sym_eq in H1].
+1,3: contradict H1; apply HT', HA; easy.
+apply ord_inj; easy.
+Qed.
+
+Lemma sortedF_sortedF_S :
+  forall {n} {A : 'I_n -> T}, sortedF A -> sortedF_S A.
+Proof. move=>> HA i Hi1; apply HA; apply /ltP; apply ltnSn. Qed.
+
+(* leT is assumed transitive. *)
+Lemma sortedF_S_sortedF_aux :
+  forall {n} {A : 'I_n -> T},
+    (forall x y z, leT x y -> leT y z -> leT x z) ->
+    (forall p (i : 'I_n) (H : i + p + 1 < n), leT (A i) (A (Ordinal H))) ->
+    sortedF A.
+Proof.
+intros n A HT HA i j H1.
+assert (H2 : i <= j) by now apply /leP; apply Nat.lt_le_incl.
+assert (H3 : i + (j - i - 1) + 1 = j).
+  rewrite addnBA; [| rewrite subn_gt0; apply /ltP; easy].
+  rewrite subnK; rewrite subnKC//.
+  apply leq_ltn_trans with i; [| apply /ltP]; easy.
+assert (Hj : (i + (j - i - 1) + 1 < n)) by now rewrite H3.
+replace j with (Ordinal Hj); [apply HA |].
+apply ord_inj; easy.
+Qed.
+
+(* leT is assumed transitive. *)
+Lemma sortedF_S_sortedF :
+  forall {n} {A : 'I_n -> T},
+    (forall x y z, leT x y -> leT y z -> leT x z) ->
+    sortedF_S A -> sortedF A.
+Proof.
+intros n A HT HA; apply (sortedF_S_sortedF_aux HT).
+apply (strong_induction (fun p => forall i H, leT (A i) (A (Ordinal H)))).
+intros p; destruct p as [|p].
+(* *)
+intros Hp i H1.
+assert (H2 : i.+1 = i + 0 + 1) by now rewrite -addn0_sym addn1.
+assert (H3 : i.+1 < n) by now rewrite H2.
+replace (Ordinal _) with (Ordinal H3); [apply HA | apply ord_inj; easy].
+(* *)
+intros Hp i H1.
+assert (H2 : i + p + 1 < n)
+    by now apply ltn_trans with (i + p.+1 + 1); [rewrite ltn_add2r ltn_add2l |].
+apply HT with (A (Ordinal H2)).
+apply Hp; apply /ltP; easy.
+assert (H3 : (i + p + 1).+1 = i + p.+1 + 1) by now rewrite -addnA !addn1.
+assert (H4 : (i + p + 1).+1 < n) by now rewrite H3.
+replace (Ordinal H1) with (Ordinal H4); [apply HA | apply ord_inj; easy].
+Qed.
+
+(* leT is assumed transitive. *)
+Lemma sortedF_equiv :
+  forall {n} {A : 'I_n -> T},
+    (forall x y z, leT x y -> leT y z -> leT x z) ->
+    sortedF A <-> sortedF_S A.
+Proof.
+move=>> HT; split; [apply sortedF_sortedF_S | apply (sortedF_S_sortedF HT)].
+Qed.
+
+End Ord_compl4a.
+
+
+Section Ord_compl4b.
+
+(** Definition and properties of ord_le/ord_lt. *)
+
+Definition ord_le {n} : 'I_n -> 'I_n -> Prop := fun i j => (i <= j)%coq_nat.
+Definition ord_lt {n} : 'I_n -> 'I_n -> Prop := fun i j => (i < j)%coq_nat.
+
+Lemma ord_le_refl : forall {n} (i : 'I_n), ord_le i i.
+Proof. intros; apply Nat.le_refl. Qed.
+
+Lemma ord_le_antisym :
+  forall {n} (i j : 'I_n), ord_le i j -> ord_le j i -> i = j.
+Proof. intros; apply ord_inj, Nat.le_antisymm; easy. Qed.
+
+Lemma ord_le_trans :
+  forall {n} (i j k : 'I_n), ord_le i j -> ord_le j k -> ord_le i k.
+Proof. move=>>; apply Nat.le_trans. Qed.
+
+Lemma ord_le_total : forall {n} (i j : 'I_n), ord_le i j \/ ord_le j i.
+Proof. intros; apply nat_le_total. Qed.
+
+Lemma ord_lt_irrefl : forall {n} (i : 'I_n), ~ ord_lt i i.
+Proof. intros; apply Nat.lt_irrefl. Qed.
+
+Lemma ord_lt_asym :
+  forall {n} (i j : 'I_n), ord_lt i j -> ~ ord_lt j i.
+Proof. move=>>; apply Nat.lt_asymm. Qed.
+
+Lemma ord_lt_trans :
+  forall {n} (i j k : 'I_n), ord_lt i j -> ord_lt j k -> ord_lt i k.
+Proof. move=>>; apply Nat.lt_trans. Qed.
+
+Lemma ord_lt_total_strict :
+  forall {n} (i j : 'I_n), i <> j -> ord_lt i j \/ ord_lt j i.
+Proof. intros; apply nat_lt_total_strict, ord_neq_compat; easy. Qed.
+
+(** Definition and properties of ord_leq/ord_ltn. *)
+
+Definition ord_leq {n} : rel 'I_n := fun i j => i <= j.
+Definition ord_ltn {n} : rel 'I_n := fun i j => i < j.
+
+Lemma ord_leq_total : forall {n} (i j : 'I_n), ord_leq i j || ord_leq j i.
+Proof. intros; apply leq_total. Qed.
+
+End Ord_compl4b.
+
+
+Section Ord_compl4c.
+
+(** Definition and properties of sortedF. *)
+
+Definition incrF {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF ord_lt f.
+Definition incrF_S {n1 n2} (f : 'I_{n1,n2}) : Prop := sortedF_S ord_lt f.
+
+Lemma incrF_nil : forall {n} (f : 'I_{0,n}), incrF f.
+Proof. intros; apply sortedF_nil. Qed.
+
+Lemma incrF_one : forall {n} (f : 'I_{1,n}), incrF f.
+Proof. intros; apply sortedF_one. Qed.
+
+Lemma incrF_inj :
+  forall {n1 n2} {f : 'I_{n1,n2}}, incrF f -> injective f.
+Proof. move=>>; apply sortedF_inj, ord_lt_irrefl. Qed.
+
+Lemma incrF_equiv : forall {n1 n2} (f : 'I_{n1,n2}), incrF f <-> incrF_S f.
+Proof. intros; apply sortedF_equiv, ord_lt_trans. Qed.
+
+Lemma incrF_comp :
+  forall {n1 n2 n3} {f : 'I_{n1,n2}} {g : 'I_{n2,n3}},
+    incrF f -> incrF g -> incrF (g \o f).
+Proof. move=>> Hf Hg i1 j1 H1; apply Hg, Hf; easy. Qed.
+
+End Ord_compl4c.
+
+
 Section Cast_ord.
 
 (* Properties of cast_ord. *)
diff --git a/FEM/multi_index.v b/FEM/multi_index.v
index bd18f8b5769831c25ec5017b27d27394aa34fd59..30cc405175cbd4ff903dfbaf3912f18f81b44282 100644
--- a/FEM/multi_index.v
+++ b/FEM/multi_index.v
@@ -11,38 +11,9 @@ From Lebesgue Require Import Subset Function.
 
 From FEM Require Import Compl Algebra binomial geometry.
 
-(*Local Open Scope nat_scope.*)
-
 
 Section lexico_MO.
 
-(*
-Definition MO2 (x y : 'nat^2) : Prop :=
-  ((x ord0 + x ord_max)%coq_nat < (y ord0 + y ord_max)%coq_nat)%coq_nat
-  \/
-  (((x ord0 + x ord_max)%coq_nat = (y ord0 + y ord_max)%coq_nat) /\ (x ord_max < y ord_max)%coq_nat).
-(*  lexico lt (coupleF (x ord0 + x ord_max)%coq_nat (x ord_max))
-         (coupleF (y ord0 + y ord_max)%coq_nat (y ord_max)).*)
-
-(* (0,0) < (n,0) *)
-Lemma MO2_aux1 : forall n : nat, (0 < n)%coq_nat -> MO2 (coupleF 0 0) (coupleF n 0).
-Proof.
-intros n Hn; unfold MO2.
-repeat rewrite coupleF_0 coupleF_1.
-rewrite 2!Nat.add_0_r.
-left; easy.
-Qed.
-
-(* (n,0) < (0,n) *)
-Lemma MO2_aux2 : forall n : nat, (0 < n)%coq_nat -> MO2 (coupleF n 0) (coupleF 0 n).
-Proof.
-intros n Hn; unfold MO2. 
-repeat rewrite coupleF_0 coupleF_1.
-rewrite Nat.add_0_r Nat.add_0_l.
-right; easy.
-Qed.
-*)
-
 Fixpoint MOn {n} (x y : 'nat^n) : Prop :=
   match n as p return (n = p -> _) with
     | 0 => fun H => False
@@ -56,23 +27,40 @@ Proof.
 intros n x y H; simpl; left; easy.
 Qed.
 
-
-Lemma MOn_aux1 : forall x y : 'nat^1, MOn x y = (x ord0 < y ord0)%coq_nat.
+Lemma MOn_correct1 : forall x y : 'nat^1, MOn x y = (x ord0 < y ord0)%coq_nat.
 Proof.
 intros x y; simpl; rewrite 2!sum_1.
-assert (H : forall P Q, (P \/ Q /\ False) = P).
-  intros; apply PropExtensionality.propositional_extensionality; tauto.
+assert (H : forall P Q, (P \/ Q /\ False) = P)
+    by (intros; apply propositional_extensionality; tauto).
 apply H.
 Qed.
 
 (*
-Lemma MOn_aux2 : forall x y : 'nat^2, MOn x y = MO2 x y.
+Definition MO2 (x y : 'nat^2) : Prop :=
+  ((x ord0 + x ord_max)%coq_nat < (y ord0 + y ord_max)%coq_nat)%coq_nat
+  \/
+  (((x ord0 + x ord_max)%coq_nat = (y ord0 + y ord_max)%coq_nat) /\ (x ord_max < y ord_max)%coq_nat).
+(*  lexico lt (coupleF (x ord0 + x ord_max)%coq_nat (x ord_max))
+         (coupleF (y ord0 + y ord_max)%coq_nat (y ord_max)).*)
+
+(* (0,0) < (n,0) *)
+Lemma MO2_correct1 : forall n : nat, (0 < n)%coq_nat -> MO2 (coupleF 0 0) (coupleF n 0).
+Proof.
+intros; unfold MO2; rewrite !coupleF_0 !coupleF_1 2!Nat.add_0_r; left; easy.
+Qed.
+
+(* (n,0) < (0,n) *)
+Lemma MO2_correct2 : forall n : nat, (0 < n)%coq_nat -> MO2 (coupleF n 0) (coupleF 0 n).
 Proof.
-intros x y; simpl.
-rewrite 2!sum_coupleF 2!castF_refl 2!skipF_coupleF_0 2!sum_singleF 2!singleF_0.
+intros; unfold MO2; rewrite !coupleF_0 !coupleF_1 Nat.add_0_r Nat.add_0_l; right; easy.
+Qed.
+
+Lemma MOn_correct2 : forall x y : 'nat^2, MOn x y = MO2 x y.
+Proof.
+intros x y; simpl; rewrite !sum_2 !sum_1 !castF_refl !skipF_2l !singleF_0.
 unfold MO2; f_equal.
-assert (H : forall P Q R, (P /\ (Q \/ R /\ False)) = (P /\ Q)).
-  intros; apply PropExtensionality.propositional_extensionality; tauto.
+assert (H : forall P Q R, (P /\ (Q \/ R /\ False)) = (P /\ Q))
+    by (intros; apply propositional_extensionality; tauto).
 apply H.
 Qed.
 *)
@@ -97,7 +85,6 @@ now rewrite H3.
 apply IHn with (1:=H4); easy.
 Qed.
 
-
 Lemma MOn_asym : forall  {n} (x y:'nat^n), 
     MOn x y -> MOn y x -> False.
 Proof.
@@ -116,43 +103,33 @@ intros (H5,H6).
 apply IHn with (1:=H4); easy.
 Qed.
 
-Lemma MOn_total_order : forall  {n} (x y:'nat^n), 
-   MOn x y \/ MOn y x \/ x = y.
+Lemma MOn_irrefl : forall {n} (x : 'nat^n), ~ MOn x x.
+Proof. intros n x H; apply (MOn_asym x x); easy. Qed.
+
+Lemma MOn_total_strict :
+  forall  {n} (x y : 'nat^n), x <> y -> MOn x y \/ MOn y x.
 Proof.
 intros n; induction n.
-simpl; intros x y; right; right.
-apply hat0F_singl.
-intros x y.
-case (Nat.le_gt_cases (sum x) (sum y)); intros H.
-case (proj1 (Nat.lt_eq_cases _ _) H); intros H1.
+simpl; intros x y H; contradict H; apply hat0F_singl.
+intros x y H; destruct (lt_eq_lt_dec (sum x) (sum y)) as [[H1 | H1] | H1].
 (* sum x < sum y *)
 left; simpl; left; easy.
-(* sum y < sum x *)
-2: right; left; simpl; left; easy.
 (* sum x = sum y *)
-specialize (IHn (skipF x ord0) (skipF y ord0)).
-simpl; rewrite 2!castF_refl.
-case IHn; intros H2.
+assert (H2 : skipF x ord0 <> skipF y ord0).
+  contradict H; apply extF_skipF with ord0; [| easy].
+  apply nat_plus_reg_r with (sum (skipF x ord0)).
+  rewrite <- (sum_skipF x), H, <- (sum_skipF y); easy.
+simpl; rewrite !castF_refl.
+destruct (IHn (skipF x ord0) (skipF y ord0) H2) as [H3 | H3].
 left; right; easy.
-case H2; intros H3.
-right; left; right; easy.
-(* full equality case *)
-right; right.
-apply extF_skipF with ord0; try easy.
-apply nat_plus_reg_r with (sum (skipF x ord0)).
-rewrite <- (sum_skipF x).
-rewrite H3; rewrite <- (sum_skipF y); easy.
-Qed.
-
-Lemma MOn_neq : forall {n} (x y:'nat^n), MOn x y -> x <> y.
-Proof.
-intros n x y H1 H2.
-apply (MOn_asym x y); try easy.
-subst; easy.
+right; right; easy.
+(* sum y < sum x *)
+right; simpl; left; easy.
 Qed.
 
 End lexico_MO.
 
+
 Section MI_defs.
 
 Definition Slice_op {d:nat} (i:nat)  
@@ -160,8 +137,6 @@ Definition Slice_op {d:nat} (i:nat)
           castF (add1n d) (concatF (singleF i) alpha).
     (* of type 'nat^(d.+ 1) *)
 
-
-
 Lemma Slice_op_sum: forall d k i (alpha:'nat^d),
    (i <= k)%coq_nat -> (sum alpha = k-i)%coq_nat -> sum (Slice_op i alpha) = k.
 Proof.
@@ -173,7 +148,6 @@ unfold plus; simpl; unfold m_plus; simpl.
 auto with arith zarith.
 Qed.
 
-
 (* exists unique, useful? *)
 Lemma Slice_op_correct : forall {d:nat} k (alpha: 'nat^(d.+1)),
     sum alpha = k ->
@@ -204,8 +178,6 @@ intros V; unfold liftF_S; simpl; f_equal.
 apply ord_inj; simpl; unfold bump; simpl; auto with arith.
 Qed.
 
-
-
 Definition Slice_fun {d n:nat} (u:nat) (a:'I_n -> 'nat^d) : 'I_n -> 'nat^(d.+1)
    := mapF (Slice_op u) a.
 
@@ -223,7 +195,6 @@ intros V; f_equal.
 apply ord_inj; simpl; unfold bump; simpl; auto with arith.
 Qed.
 
-
 Lemma MOn_Slice_fun_aux : forall {d n} u (alpha:'I_n -> 'nat^d)
      (i j:'I_n), (i < j)%coq_nat ->
      MOn (alpha i) (alpha j) -> 
@@ -251,18 +222,14 @@ now rewrite Nat.add_sub.
 rewrite 2!Slice_fun_skipF0; easy.
 Qed.
 
-
-
 Lemma MOn_Slice_fun : forall {d n} u (alpha:'I_n -> 'nat^d),
-   is_orderedF MOn alpha -> is_orderedF MOn (Slice_fun u alpha).
+   sortedF MOn alpha -> sortedF MOn (Slice_fun u alpha).
 Proof.
 intros d n u alpha H i j H1.
 apply MOn_Slice_fun_aux; try easy.
 apply H; easy.
 Qed.
 
-
-
 Definition pbinom a b := (binom (a+b)%coq_nat a).-1.
 
 Lemma pbinom_eq : forall a b, 
@@ -322,13 +289,11 @@ rewrite pbinom_eq.
 apply binom_gt_0; auto with arith.
 Qed.
 
-
 (* was
 Lemma C_d_k_aux : forall (d k :nat),
   sum (succF (fun i : 'I_k.+1 => (pbinom i d.-1)))
      = (pbinom k (d.+1.-1)).+1.
 that is wrong for d=0 *)
-
 Lemma C_d_k_aux : forall (d dd k :nat) (H:d = dd.+1),
   sum (succF (fun i : 'I_k.+1 => (pbinom i d.-1)))
      = (pbinom k (d.+1.-1)).+1.
@@ -354,8 +319,6 @@ intros d k.
 rewrite (C_d_k_aux d.+1 d k); try easy.
 Qed.
 
-
-
 Lemma C_d_k_aux2 : forall (d k:nat),
   (sum (succF (fun i : 'I_k.+1 => pbinom i d))).-1 = pbinom k d.+1.
 Proof.
@@ -364,9 +327,7 @@ rewrite -(sum_ext (succF (fun i => pbinom i (d.+1.-1)))); try easy.
 rewrite (C_d_k_aux d.+1 d k); try easy.
 Qed.
 
-
 (* \cal C^d_k *)
-
 Fixpoint C_d_k (d k :nat) {struct d} : 'I_((pbinom k d.-1).+1) -> 'nat^d
    := match d with
     | O    => fun _ _ => 0
@@ -379,12 +340,10 @@ Fixpoint C_d_k (d k :nat) {struct d} : 'I_((pbinom k d.-1).+1) -> 'nat^d
 
 (* when d=0 it is 'I_1 -> 'nat^0 *)
 
-
 (* TODO SB : 1) virer d=0 pour déf de C_d_k et patcher A
              2) changer taille de C pour d=k=0 1 ; sinon 0
 *)
 
-
 Lemma C_0_k_eq : forall k, C_d_k 0 k = fun _ _ => 0.
 Proof.
 easy.
@@ -412,7 +371,6 @@ intros d k1 k2 i1 i2 Hk Hi; subst.
 f_equal; apply ord_inj; easy.
 Qed.
 
-
 Lemma C_d_k_sum : forall d k i, (0 < d)%coq_nat -> sum (C_d_k d k i) = k.
 Proof.
 intros d; case d.
@@ -439,7 +397,6 @@ apply sym_eq, Nat.add_sub_eq_l.
 auto with arith zarith.
 Qed.
 
-
 Lemma C_d_0_eq : forall d, C_d_k d 0 = fun _ => constF d 0.
 Proof.
 intros d; case d.
@@ -464,7 +421,6 @@ intros d Hd; unfold pbinom.
 rewrite binom_n1; auto with arith zarith.
 Qed.
 
-
 Lemma C_d_1_eq : forall d (Hd: (0 < d)%coq_nat),
   C_d_k d 1 =  castF (C_d_1_eq_aux d Hd) (itemF d 1).
 Proof.
@@ -522,7 +478,6 @@ apply ord_inj; easy.
 apply ord_inj; easy.
 Qed.
 
-
 Lemma C_d_k_head : forall d k,
    C_d_k d.+1 k ord0 = itemF d.+1 k ord0.
 Proof.
@@ -549,7 +504,6 @@ rewrite fct_zero_eq.
 rewrite itemF_correct_r; try easy.
 Qed.
 
-
 Lemma C_d_k_last : forall d k,
    C_d_k d.+1 k ord_max = itemF d.+1 k ord_max.
 Proof.
@@ -603,19 +557,19 @@ unfold plus; simpl.
 apply Nat.add_lt_mono_r; auto with arith.
 Qed.
 
-Lemma C_d_k_MOn : forall d k, (0 < d)%coq_nat -> is_orderedF MOn (C_d_k d k).
+Lemma C_d_k_MOn : forall d k, (0 < d)%coq_nat -> sortedF MOn (C_d_k d k).
 Proof.
 intros d; case d.
 intros k H; contradict H; auto with arith.
 clear d; intros d k _; generalize k; clear k; induction d.
-intros k; unfold is_orderedF.
+intros k; unfold sortedF.
 simpl; unfold pbinom; rewrite Nat.add_0_r binom_nn.
 replace (1.-1.+1) with 1 by auto with arith.
 intros i j H.
 contradict H; rewrite 2!ord1; auto with arith.
 (* *)
 intros k; rewrite C_d_k_eq.
-apply is_orderedF_castF.
+apply sortedF_castF.
 apply concatnF_order.
 apply MOn_trans.
 intros i.
@@ -654,7 +608,6 @@ rewrite 2!singleF_0.
 rewrite bump_r; auto with zarith.
 Qed.
 
-
 Lemma C_d_k_surj : forall d k,  forall b : 'nat^d, 
    (0 < d)%coq_nat ->
     sum b = k -> exists i, b = C_d_k d k i.
@@ -696,7 +649,6 @@ apply sym_eq, Nat.add_sub_eq_l; auto with arith zarith.
 apply Nat.sub_add; easy.
 Qed.
 
-
 Lemma A_d_k_aux : forall d k dd, (d = dd.+1) ->
    sum (fun i : 'I_k.+1 => (pbinom i (d.-1)).+1)
         = (pbinom d k).+1.
@@ -735,7 +687,6 @@ auto with arith.
 f_equal; auto with zarith.
 Qed.
 
-
 Lemma A_d_Sk_eq : forall d k,
     A_d_k d.+1 k.+1 
        = castF (A_d_Sk_eq_aux d k) (concatF (A_d_k d.+1 k)  (C_d_k d.+1 k.+1)).
@@ -831,7 +782,6 @@ apply Nat.le_trans with (2:= A_d_k_sum d k i).
 apply sum_le_one_nat.
 Qed.
 
-
 Lemma A_d_k_surj : forall d k (b:'nat^d),
    (sum b <= k)%coq_nat -> exists i, b = A_d_k d k i.
 Proof.
@@ -856,9 +806,8 @@ rewrite concatn_ord_correct.
 easy.
 Qed.
 
-
 Lemma A_d_k_MOn : forall d k,
-    is_orderedF MOn (A_d_k d k).
+    sortedF MOn (A_d_k d k).
 Proof.
 intros d; case d; clear d.
 intros k; intros i j Hij.
@@ -870,7 +819,7 @@ assert ( m < 1)%coq_nat by now apply /ltP.
 auto with zarith.
 (* *)
 intros d k; unfold A_d_k.
-apply is_orderedF_castF.
+apply sortedF_castF.
 apply concatnF_order.
 apply MOn_trans.
 intros i; apply C_d_k_MOn; auto with arith.
@@ -880,16 +829,14 @@ rewrite C_d_k_sum; auto with arith.
 rewrite C_d_k_sum; auto with arith.
 Qed.
 
-
 Lemma A_d_k_inj :  forall d k,
     injective (A_d_k d k).
 Proof.
-intros d k; apply is_orderedF_inj with MOn.
-apply MOn_neq.
+intros d k; apply sortedF_inj with MOn.
+apply MOn_irrefl.
 apply A_d_k_MOn.
 Qed.
 
-
 Definition A_d_k_inv (d k:nat) (b:'nat^d) : 'I_((pbinom d k).+1) :=
    match (le_dec (sum b) k) with
      | left H => 
@@ -967,7 +914,6 @@ rewrite {2}(pbinom_eq 1 k.+1); unfold pbinom at 3.
 rewrite binom_n1; auto with arith zarith.
 Qed.
 
-
 (** "Livre Vincent Definition 1540 - p18." *)
 Lemma A_1_k_eq : forall k,
   A_d_k 1 k = constF 1.
@@ -1115,4 +1061,3 @@ rewrite sum_itemF; easy.
 Qed.
 
 End MI_defs.
-