diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 2de3be349f4d986a13ecf5988b3bf9dcfb05da77..7fff7214b5ec725e736248195e1fd6572d0df5d5 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -1511,30 +1511,22 @@ assert (Hlf'b : lf' = map (f \o p1) (ord_enum n1.+1)).
   rewrite nth_ord_enum; easy.
   1,2,3: rewrite size_ord_enum; easy.
 (* *)
-exists p1; split; [apply injF_bij; easy |].
-move=> i1 j1 /ltn_equiv [H1 H2]; rewrite !comp_correct.
+exists p1; split; [apply injF_bij; easy | apply incrF_equiv].
+intros i1 Hj1; rewrite !comp_correct; pose (j1 := Ordinal Hj1); fold j1.
+assert (H : i1 < j1) by easy.
+destruct (proj1 ltn_equiv H) as [H1 H2].
 apply leq_neq_ltn;
     [| apply ord_neq_compat, (inj_contra Hf), (inj_contra Hp1a), ord_neq; easy].
-assert (Hi1 : i1 < n1.+1) by now destruct i1.
-assert (Hj1 : j1 < n1.+1) by now destruct j1.
-assert (Hi1' : i1.+1 < n1.+1)
-    by now apply (ltn_S j1); [apply leq_neq_ltn |]; easy.
-move: (sort_sorted ord_leq_total lf); rewrite Hp1b(*; fold lf'*).
-replace (sorted _ _) with (sorted ord_leq (map (f \o p1) (ord_enum n1.+1))).
-2: do 2 f_equal ; apply extF; intros k1; rewrite Hlf; easy.
-move=> /sortedP. (*rewrite Hlf'a; intros Hlfa.
-specialize (Hlfa ord0 i1 Hi1').*)
-
-
-
-
-
-(*
-ltn_sorted_uniq_leq : sorted ltn s = uniq s && sorted leq s
-nth_mkseq : i < n -> nth x0 (mkseq f n) i = f i
-*)
-
-Admitted.
+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].
+move=> /(sortedP ord0) => H3; specialize (H3 (nat_of_ord i1) Hj1b); move: H3.
+replace (nth _ _ i1.+1) with (nth ord0 lf' j1); [| easy].
+rewrite Hlf'b !(nth_map ord0); [| rewrite size_ord_enum; easy..].
+rewrite !comp_correct !nth_ord_enum; easy.
+Qed.
 
 (*
 Lemma nth_correct :
diff --git a/FEM/Algebra/nat_compl.v b/FEM/Algebra/nat_compl.v
index 1968e93f62c9d84908ff7b0b4bd02d7c96566ec5..c7421fabee6c823c0eb531e952c5742124c87479 100644
--- a/FEM/Algebra/nat_compl.v
+++ b/FEM/Algebra/nat_compl.v
@@ -324,7 +324,7 @@ destruct (le_lt_eq_dec _ _ Hi1) as [Hi3 | Hi3]; [| contradict Hi2]; easy.
 Qed.
 
 Lemma ltn_leq_neq : forall {n i}, i < n -> i <= n /\ i <> n.
-Proof. move=>> /ltP Hi; split; [apply /leP |]; auto with zarith. Qed.
+Proof. intros; split; [apply ltnW | apply ltn_neq]; easy. Qed.
 
 Lemma ltn_equiv : forall {n i}, i < n <-> i <= n /\ i <> n.
 Proof.
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index d845d2c2f6a7434a9487cbdb80583affacc1157a..3df1f52d9b4a816ed6d0f39e7920295b40a3e792 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -759,9 +759,34 @@ 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;