diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 06ea1284409b94eafa10ce0d45d8e3795586bc4c..a088df6d580596af4de2b3104da289e96c102108 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -1538,6 +1538,7 @@ rewrite -Hp'2; unfold f'; rewrite widen_narrow_S.
 contradict Hi1; apply Hf; easy.
 Qed.
 
+(* A MONTRER B0 *)
 Lemma injF_restr_bij_EX :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
     { p1 : 'I_[n1] | bijective p1 /\ incrF (f \o p1) }.
@@ -1575,9 +1576,9 @@ assert (Hi1a : i1 < n1.+1) by now destruct i1.
 assert (Hj1a : j1 < n1.+1) by now destruct j1.
 assert (Hj1b : j1 < size lf') by now rewrite Hlf'a.
 move: (sort_sorted ord_leq_total lf); rewrite Hp1b.
-replace (sorted _ _) with (sorted ord_leq lf'); [| f_equal].
+replace (sorted _ _) with (sorted ord_leq lf') by easy.
 move=> /(sortedP ord0) => H3; specialize (H3 (nat_of_ord i1) Hj1b); move: H3.
-replace (nth _ _ i1.+1) with (nth ord0 lf' j1); [| easy].
+replace (nth _ _ i1.+1) with (nth ord0 lf' j1) by easy.
 rewrite Hlf'b !(nth_map ord0); [| rewrite size_ord_enum; easy..].
 rewrite !comp_correct !nth_ord_enum; easy.
 Qed.
@@ -4885,6 +4886,7 @@ contradict Hi2; rewrite not_all_not_ex_equiv.
 destruct (HP i2) as [[i1 Hi1] | Hi2]; [exists i1 |]; easy.
 Qed.
 
+(* A MONTRER A2b *)
 Lemma filterP_ord_Rg :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f)
       {P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2),
@@ -4926,7 +4928,8 @@ apply Nat.lt_le_incl, Hf; simpl.
 apply Nat.neq_0_lt_0, (ord_neq_compat Ht).
 Qed.
 
-Lemma ext_fun_incrF_Rg :
+(* A MONTRER A2a *)
+ Lemma fun_ext_incrF_Rg :
   forall {n1 n2} {f g : 'I_{n1,n2}},
     incrF f -> incrF g -> Rg f = Rg g -> f = g.
 Proof.
@@ -4943,18 +4946,20 @@ 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.
 
+(* A MONTRER A1b *)
 Lemma filterP_ord_w_incrF :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f) {P1 : 'Prop^n1}
       {P2 : 'Prop^n2} (HP : extendPF f P1 P2),
     let H := lenPF_extendPF (incrF_inj Hf) HP in
     f \o filterP_ord = filterP_ord \o (cast_ord H).
 Proof.
-intros; apply ext_fun_incrF_Rg.
+intros; apply fun_ext_incrF_Rg.
 apply incrF_comp; [apply filterP_ord_incrF | easy].
 apply filterP_cast_ord_incrF.
 apply filterP_ord_Rg.
 Qed.
 
+(* A MONTRER A1a *)
 Lemma filterP_f_ord_w_incrF :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f)
       {P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2)
@@ -5024,6 +5029,7 @@ rewrite HA2; [ apply maskPF_correct_r; rewrite -Rg_compl_equiv |];
     rewrite Rg_compl; easy.
 Qed.
 
+(* A MONTRER A0 *)
 Lemma filterPF_unfunF :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
       {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop} (HP : extendPF f P1 P2)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 15554a9e10abf47875f4939f808c13b453a84cc9..0043062536f08f5a622048881333b46556b04caf 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -122,8 +122,9 @@ Section Seq_compl3.
 
 Context {T : eqType}.
 
+(* A MONTRER B3b *)
 Lemma injS_equiv_seq :
-  forall {P : pred T} {sT : subType (T:=T) P} {f : T -> sT},
+  forall {P : pred T} {sT : subType P} {f : T -> sT},
     injS P f <-> forall s, all P s -> { in s &, injective f }.
 Proof.
 move=>>; split.
@@ -620,6 +621,7 @@ Qed.
 Lemma nth_ord_enum : forall {n} i0 {i : 'I_n}, nth i0 (ord_enum n) i = i.
 Proof. intros n i0 [j Hj]; apply nth_ord_enum_alt. Qed.
 
+(* A MONTRER B2b  *)
 Lemma map_nth_ord_enum :
   forall (l : seq T),
     map (fun i : 'I_(size l) => nth x0 l i) (ord_enum (size l)) = l.
@@ -628,6 +630,7 @@ intros l; move: (map_nth_iota0 x0 (leqnn (size l))).
 rewrite take_size -val_ord_enum -map_comp; easy.
 Qed.
 
+(* A MONTRER B2c *)
 Lemma map_nth_invF :
   forall {n l1 l2}, size l1 = n.+1 -> size l2 = n.+1 ->
     forall {p : 'I_[n.+1]} (Hp : injective p),
@@ -678,6 +681,7 @@ move=>> Hj1 Hj2; rewrite !in_ordS_correct_l_alt.
 move=> /(f_equal (@nat_of_ord _)); easy.
 Qed.
 
+(* A MONTRER B3a *)
 Lemma ord_enumS_eq : forall {n}, ord_enum n.+1 = map in_ordS (iota 0 n.+1).
 Proof.
 intros n; apply (@eq_from_nth _ ord0).
@@ -699,6 +703,7 @@ Context {T : Type}.
 Variable leT : rel T.
 Variable x0 : T.
 
+(* A MONTRER B2a *)
 Lemma perm_ord_enum_sort :
   forall l,
     { il | perm_eq il (ord_enum (size l)) /\ uniq il &
@@ -733,12 +738,27 @@ Section Ord_compl3b.
 Context {T : eqType}.
 Context {leT : rel T}.
 
+(* A MONTRER A4c *)
+Lemma sorted_ordP :
+  forall {l : seq T} x0 x1,
+    reflect (forall (i : 'I_(size l)) (Hi1 : i.+1 < size l),
+              leT (nth x0 l i) (nth x1 l (Ordinal Hi1)))
+            (sorted leT l).
+Proof.
+intros l x0 x1; apply (iffP (sortedP x0)); intros H.
+intros [i Hi] Hi1; simpl; rewrite (set_nth_default x0 x1)//; apply H; easy.
+intros i Hi1; rewrite (set_nth_default x1 x0 Hi1).
+assert (Hi : i < size l) by now apply ltn_trans with i.+1.
+apply (H (Ordinal Hi) Hi1).
+Qed.
+
 Hypothesis HT0 : antisymmetric leT.
 Hypothesis HT1 : transitive leT.
 Hypothesis HT2 : total leT.
 
 Variable x0 : T.
 
+(* A MONTRER B1b *)
 Lemma perm_EX :
   forall {l1 l2}, perm_eq l1 l2 ->
     { p : 'I_[size l2] | injective p &
@@ -793,6 +813,7 @@ rewrite !(nth_map ord0)//; [| rewrite size_ord_enum; easy].
 rewrite !nth_ord_enum; unfold q2; rewrite f_inv_correct_l; easy.
 Qed.
 
+(* A MONTRER B1a *)
 Lemma sort_perm_EX :
   forall l, { p : 'I_[size l] | injective p &
     sort leT l = map (fun i => nth x0 l (p i)) (ord_enum (size l)) }.
@@ -931,7 +952,7 @@ End Widen_Lift_S.
 
 Section Ord_compl4a.
 
-(** Definition and properties of sortedF. *)
+(** Definition and properties of sortedF/sortedF_S. *)
 
 Context {T : Type}.
 
@@ -979,10 +1000,10 @@ assert (H3 : i + (j - i - 1) + 1 = j).
   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.
+replace j with (Ordinal Hj); [apply HA | apply ord_inj; easy].
 Qed.
 
+(* A MONTRER A3c *)
 (* leT is assumed transitive. *)
 Lemma sortedF_S_sortedF :
   forall {n} {A : 'I_n -> T},
@@ -1008,6 +1029,7 @@ assert (H4 : (i + p + 1).+1 < n) by now rewrite H3.
 replace (Ordinal H1) with (Ordinal H4); [apply HA | apply ord_inj; easy].
 Qed.
 
+(* A MONTRER A3b *)
 (* leT is assumed transitive. *)
 Lemma sortedF_equiv :
   forall {n} {A : 'I_n -> T},
@@ -1087,12 +1109,28 @@ Lemma ord_ltn_total_strict :
   forall {n} (i j : 'I_n), i != j = ord_ltn i j || ord_ltn j i.
 Proof. move=>>; apply neq_ltn. Qed.
 
+(* A MONTRER A4b *)
+Lemma sorted_enum_ord : forall {n}, sorted ord_ltn (enum 'I_n).
+Proof.
+intros n; destruct n as [|n]; [rewrite (size0nil (size_enum_ord _)); easy |].
+apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
+unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
+Qed.
+
+(* A MONTRER A4a *)
+Lemma sorted_filter_enum_ord :
+  forall {n} (P : 'I_n -> Prop),
+    sorted ord_ltn (filter (fun i => asbool (P i)) (enum 'I_n)).
+Proof.
+intros; apply sorted_filter; [apply ord_ltn_trans | apply sorted_enum_ord].
+Qed.
+
 End Ord_compl4b.
 
 
 Section Ord_compl4c.
 
-(** Definition and properties of sortedF. *)
+(** Definition and properties of incrF/incrF_S. *)
 
 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.
@@ -1107,6 +1145,7 @@ Lemma incrF_inj :
   forall {n1 n2} {f : 'I_{n1,n2}}, incrF f -> injective f.
 Proof. move=>>; apply sortedF_inj, ord_lt_irrefl. Qed.
 
+(* A MONTRER A3a *)
 Lemma incrF_equiv : forall {n1 n2} (f : 'I_{n1,n2}), incrF f <-> incrF_S f.
 Proof. intros; apply sortedF_equiv, ord_lt_trans. Qed.
 
@@ -2275,32 +2314,7 @@ Lemma unfilterP_ord_inj :
       unfilterP_ord HP0 i = unfilterP_ord HP0 j -> i = j.
 Proof. move=>> Hi Hj; apply enum_rank_in_inj; apply /asboolP; easy. Qed.
 
-Lemma sorted_ordP :
-  forall {T : Type} {leT : rel T} {l : seq T} x0 x1,
-    reflect (forall (i : 'I_(size l)) (Hi1 : i.+1 < size l),
-        leT (nth x0 l i) (nth x1 l (Ordinal Hi1))) (sorted leT l).
-Proof.
-intros T leT l x0 x1; apply (iffP (sortedP x0)); intros H.
-intros [i Hi] Hi1; simpl; rewrite (set_nth_default x0 x1)//; apply H; easy.
-intros i Hi1; rewrite (set_nth_default x1 x0 Hi1).
-assert (Hi : i < size l) by now apply ltn_trans with i.+1.
-apply (H (Ordinal Hi) Hi1).
-Qed.
-
-Lemma sorted_enum_ord : forall {n}, sorted ord_ltn (enum 'I_n).
-Proof.
-intros n; destruct n as [|n]; [rewrite (size0nil (size_enum_ord _)); easy |].
-apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
-unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
-Qed.
-
-Lemma sorted_filter_enum_ord :
-  forall {n} (P : 'I_n -> Prop),
-    sorted ord_ltn (filter (fun i => asbool (P i)) (enum 'I_n)).
-Proof.
-intros; apply sorted_filter; [apply ord_ltn_trans | apply sorted_enum_ord].
-Qed.
-
+(* A MONTRER A2e *)
 Lemma filterP_ord_incrF_S :
   forall {n} (P : 'I_n -> Prop),
     incrF_S (fun j : 'I_(lenPF P) => filterP_ord j).
@@ -2318,10 +2332,12 @@ assert (Hjj1 : jj.+1 < size (filter (fun i => asbool (P i)) (enum 'I_n)))
 apply (H0 (enum_default j) (enum_default (Ordinal Hj1)) jj Hjj1).
 Qed.
 
+(* A MONTRER A2d *)
 Lemma filterP_ord_incrF :
   forall {n} (P : 'I_n -> Prop), incrF (fun j : 'I_(lenPF P) => filterP_ord j).
 Proof. intros; apply incrF_equiv, filterP_ord_incrF_S. Qed.
 
+(* A MONTRER A2c *)
 Lemma filterP_cast_ord_incrF :
   forall {n1 n2} {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop}
       (H : lenPF P1 = lenPF P2),