diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 7a35f023b2f9a68394ead41d1ff2f242bd0b9623..06ea1284409b94eafa10ce0d45d8e3795586bc4c 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -1552,7 +1552,8 @@ pose (lf := (map f (ord_enum n1.+1))).
 assert (Hlf : forall i : 'I_n1.+1, nth ord0 lf i = f i)
     by now intros i; rewrite (nth_map ord0);
       [rewrite nth_ord_enum | rewrite size_ord_enum].
-destruct (sort_perm_EX ord_leq ord0 lf) as [p1 Hp1a Hp1b].
+destruct (sort_perm_EX ord_leq_antisym ord_leq_trans ord_leq_total ord0 lf)
+    as [p1 Hp1a Hp1b].
 assert (Hn1 : size lf = n1.+1) by now rewrite size_map size_ord_enum.
 rewrite Hn1 in p1, Hp1a, Hp1b.
 pose (lf' := map (fun i1 => nth ord0 lf (p1 i1)) (ord_enum n1.+1)).
diff --git a/FEM/Algebra/nat_compl.v b/FEM/Algebra/nat_compl.v
index 35935264430a5e8c0ff72cb8f889bd0938ff92bd..15f5b7c31b025a4c168f829bb50431c80818964b 100644
--- a/FEM/Algebra/nat_compl.v
+++ b/FEM/Algebra/nat_compl.v
@@ -291,6 +291,9 @@ Proof. move=>> /ltP; easy. Qed.
 Lemma le_leq : forall {m n}, (m <= n)%coq_nat -> m <= n.
 Proof. move=>> /leP; easy. Qed.
 
+Lemma ltn_asym : forall m n, m < n < m = false.
+Proof. move=>>; rewrite !ltnNge -negb_or; apply negbF, leq_total. Qed.
+
 (* TODO FC (01/02/2024): rename -> ltn_2_dec. *)
 Lemma lt_2_dec : forall {n}, n < 2 -> {n = 0} + {n = 1}.
 Proof.
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index ad89ce59fbfc8c23cdd7044955d82935a2cde6d9..72cc88f2327b4d25d04222a944d79ee7a1e862e5 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -1031,9 +1031,32 @@ Proof. intros; apply nat_lt_total_strict, ord_neq_compat; easy. Qed.
 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_refl : forall {n}, reflexive (@ord_leq n).
+Proof. move=>>; apply leqnn. Qed.
+
+Lemma ord_leq_antisym : forall {n}, antisymmetric (@ord_leq n).
+Proof. move=>> H; apply ord_inj, anti_leq; easy. Qed.
+
+Lemma ord_leq_trans : forall {n}, transitive (@ord_leq n).
+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.
 
+Lemma ord_ltn_irrefl : forall {n}, irreflexive (@ord_ltn n).
+Proof. move=>>; apply ltnn. Qed.
+
+Lemma ord_ltn_asym :
+  forall {n} (i j : 'I_n), ord_ltn i j && ord_ltn j i = false.
+Proof. move=>>; apply ltn_asym. Qed.
+
+Lemma ord_ltn_trans : forall {n}, transitive (@ord_ltn n).
+Proof. move=>>; apply ltn_trans. Qed.
+
+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.
+
 End Ord_compl4b.