diff --git a/FEM/Compl/Binary_relation.v b/FEM/Compl/Binary_relation.v
index a2b855836670f6596b74648cf5675f438c68f082..d16023ef7ceabb50f984cd7e0d3b15e951ed513a 100644
--- a/FEM/Compl/Binary_relation.v
+++ b/FEM/Compl/Binary_relation.v
@@ -83,23 +83,26 @@ COPYING file for more details.
  Lexicographic orders are generalizations, and variants, of the alphabetical
  order in dictionaries to finite families of any type.
 
+ Let [P : Prop]. ([True] means reflexive, and [False] means irreflexive.)
  Let [n : nat].
 
- - [lex R] is the binary relation defined for all [x y : 'T^n] by
+ - [lex R P] is the binary relation defined for all [x y : 'T^n] by
    [R (x i) (y i)] for the first index [j] such that [x j <> y j].
 
- - [colex R] is the binary relation defined for all [x y : 'T^n] by
+ - [colex R P] is the binary relation defined for all [x y : 'T^n] by
    [R (x i) (y i)] for the last index [j] such that [x j <> y j],
    ie words of the dictionary are sorted from their last letter.
 
- - [symlex R] is the converse of [lex R],
+ - [symlex R P] is the converse of [lex R],
    ie it is defined for all [x y : 'T^n] by [R (y i) (x i)] for the first index
    [j] such that [x j <> y j].
 
- - [revlex R] is the converse of [colex R],
+ - [revlex R P] is the converse of [colex R],
    ie it is defined for all [x y : 'T^n] by [R (y i) (x i)] for the last index
    [j] such that [x j <> y j].
 
+ - [*lexT] (resp. [*lexF]) are partial applications with [P := True] (resp. [P := False]).
+
  * Used logic axioms
 
  - decidability of equality in type [T] is assumed for a few results.
@@ -480,7 +483,7 @@ Section Homogeneous_binary_relation_Facts4a.
 Context {T : Type}.
 Variable R : T -> T -> Prop.
 
-(** Compatibility results with the converse operation. *)
+(** With the converse operation. *)
 
 Lemma refl_conv : reflexive R -> reflexive (converse R).
 Proof. easy. Qed.
@@ -506,7 +509,7 @@ Proof. intros H x y; rewrite eq_sym_equiv; apply H. Qed.
 Lemma str_conn_conv : strongly_connected R -> strongly_connected (converse R).
 Proof. intros H x y; apply (H y x). Qed.
 
-(** Compatibility results with the complementary operation. *)
+(** With the complementary operation. *)
 
 Lemma refl_compl_equiv :
   forall (R : T -> T -> Prop), reflexive (complementary R) <-> irreflexive R.
@@ -520,7 +523,7 @@ Lemma sym_compl :
   forall (R : T -> T -> Prop), symmetric R -> symmetric (complementary R).
 Proof. intros R1 H x y; rewrite -contra_equiv; apply H. Qed.
 
-(** Compatibility results with the comparable / incomparable operations. *)
+(** With the comparable / incomparable operations. *)
 
 Lemma compar_refl_equiv :
   forall (R : T -> T -> Prop), reflexive (comparable R) <-> reflexive R.
@@ -578,12 +581,12 @@ End Homogeneous_binary_relation_Facts4a.
 
 Section Homogeneous_binary_relation_Facts4b.
 
-(** More results about homogeneous binary relations. *)
+(** Compatibility results of compound properties of
+ homogeneous binary relations. *)
 
 Context {T : Type}.
 
-(** Compatibility results of compound properties
- with the converse operation. *)
+(** With the converse operation. *)
 
 Lemma partial_equivalence_relation_conv :
   forall (R : T -> T -> Prop),
@@ -697,8 +700,7 @@ Proof.
 intros R; split; [rewrite -{2}(conv_invol R) |]; apply strict_total_order_conv.
 Qed.
 
-(** Compatibility results of compound properties
- with the complementary operation. *)
+(** With the complementary operation. *)
 
 (* FIXME: is that true?
 Lemma total_preorder_compl :
@@ -734,8 +736,7 @@ Proof.
 intros; rewrite strict_weak_order_conv_equiv; apply strict_weak_order_compl.
 Qed. *)
 
-(** Compatibility results of compound properties
- with the comparable / incomparable operations. *)
+(** With the comparable / incomparable operations. *)
 
 Lemma equiv_rel_incompar :
   forall (R : T -> T -> Prop),
@@ -758,7 +759,7 @@ Qed.
 End Homogeneous_binary_relation_Facts4b.
 
 
-Section Lex_order_Def.
+Section Lex_orders_Def.
 
 Context {T : Type}.
 
@@ -851,10 +852,10 @@ Proof.
 intros P n x y; simpl; repeat rewrite castF_refl; rewrite eq_sym_equiv; easy.
 Qed.
 
-End Lex_order_Def.
+End Lex_orders_Def.
 
 
-Section Lex_order_Facts.
+Section Lex_orders_Facts.
 
 Context {T : Type}.
 
@@ -864,7 +865,9 @@ Hypothesis HT : eq_dec T.
 
 Variable R : T -> T -> Prop.
 
-(** Compatibility with elementary properties. *)
+(** Compatibility results with elementary properties. *)
+
+(** With reflexive. *)
 
 Lemma lexT_refl : forall n, reflexive (@lexT _ R n).
 Proof.
@@ -884,6 +887,8 @@ Proof. intros; apply refl_conv, lexT_refl; easy. Qed.
 Lemma revlexT_refl : forall n, reflexive (@revlexT _ R n).
 Proof. intros; apply refl_conv, colexT_refl; easy. Qed.
 
+(** With irreflexive. *)
+
 Lemma lexF_irrefl : forall n, irreflexive (@lexF _ R n).
 Proof.
 intros n; induction n; intros x; [easy | unfold lexF].
@@ -904,6 +909,8 @@ Proof. intros; apply irrefl_conv, lexF_irrefl; easy. Qed.
 Lemma revlexF_irrefl : forall n, irreflexive (@revlexF _ R n).
 Proof. intros; apply irrefl_conv, colexF_irrefl; easy. Qed.
 
+(** With antisymmetric. *)
+
 Lemma lexT_antisym : antisymmetric R -> forall n, antisymmetric (@lexT _ R n).
 Proof.
 intros H1 n x y; induction n; [rewrite (hat0F_unit x y); easy | unfold lexT].
@@ -933,6 +940,40 @@ Lemma revlexT_antisym :
   antisymmetric R -> forall n, antisymmetric (@revlexT _ R n).
 Proof. intros; apply antisym_conv, colexT_antisym; easy. Qed.
 
+(** With asymmetric. *)
+
+Lemma lexF_asym : asymmetric R -> forall n, asymmetric (@lexF _ R n).
+Proof.
+intros H1 n x y; induction n; [rewrite (hat0F_unit x y); easy | unfold lexF].
+rewrite !lex_S; intros [[H2a H2b] | [H2a H2b]];
+    rewrite not_or_equiv !not_and_equiv NNPP_equiv; split.
+right; apply H1; easy.
+left; apply neq_sym_equiv; easy.
+left; easy.
+right; apply IHn; easy.
+Qed.
+
+Lemma colexF_asym : asymmetric R -> forall n, asymmetric (@colexF _ R n).
+Proof.
+intros H1 n x y; induction n; [rewrite (hat0F_unit x y); easy | unfold colexF].
+rewrite !colex_S; intros [[H2a H2b] | [H2a H2b]];
+    rewrite not_or_equiv !not_and_equiv NNPP_equiv; split.
+right; apply H1; easy.
+left; apply neq_sym_equiv; easy.
+left; easy.
+right; apply IHn; easy.
+Qed.
+
+Lemma symlexF_asym :
+  asymmetric R -> forall n, asymmetric (@symlexF _ R n).
+Proof. intros; apply asym_conv, lexF_asym; easy. Qed.
+
+Lemma revlexF_asym :
+  asymmetric R -> forall n, asymmetric (@revlexF _ R n).
+Proof. intros; apply asym_conv, colexF_asym; easy. Qed.
+
+(** With transitive. *)
+
 Lemma lex_trans :
   antisymmetric R \/ asymmetric R -> transitive R ->
   forall P n, transitive (@lex _ R P n).
@@ -979,6 +1020,8 @@ Lemma revlex_trans :
   forall P n, transitive (@revlex _ R P n).
 Proof. intros; apply trans_conv, colex_trans; easy. Qed.
 
+(** With connected. *)
+
 Lemma lexF_conn_alt :
   irreflexive R -> connected_alt R -> forall n, connected_alt (@lexF _ R n).
 Proof.
@@ -1038,68 +1081,154 @@ destruct (H _ _ H2) as [H3 | H3];
 Qed.
 
 Lemma symlexF_conn : connected R -> forall n, connected (@symlexF _ R n).
-Proof. intros H n; apply conn_conv, lexF_conn; easy. Qed.
+Proof. intros; apply conn_conv, lexF_conn; easy. Qed.
 
 Lemma revlexF_conn : connected R -> forall n, connected (@revlexF _ R n).
-Proof. intros H n; apply conn_conv, colexF_conn; easy. Qed.
+Proof. intros; apply conn_conv, colexF_conn; easy. Qed.
+
+(** With strongly connected. *)
+
+(* This proof uses decidability of equality. *)
+Lemma lexT_str_conn :
+  strongly_connected R -> forall n, strongly_connected (@lexT _ R n).
+Proof.
+unfold lexT; intros H n x y; induction n.
+rewrite lex_nil; left; easy.
+rewrite !lex_S; destruct (HT (x ord0) (y ord0)) as [H1 | H1].
+destruct (IHn (skipF x ord0) (skipF y ord0)) as [H2 | H2];
+    [left | right]; right; split; easy.
+destruct (H (x ord0) (y ord0)) as [H2 | H2];
+    [left | right; rewrite neq_sym_equiv]; left; split; try easy.
+Qed.
+
+(* This proof uses decidability of equality. *)
+Lemma colexT_str_conn :
+  strongly_connected R -> forall n, strongly_connected (@colexT _ R n).
+Proof.
+unfold colexT; intros H n x y; induction n.
+rewrite colex_nil; left; easy.
+rewrite !colex_S; destruct (HT (x ord_max) (y ord_max)) as [H1 | H1].
+destruct (IHn (skipF x ord_max) (skipF y ord_max)) as [H2 | H2];
+    [left | right]; right; split; easy.
+destruct (H (x ord_max) (y ord_max)) as [H2 | H2];
+    [left | right; rewrite neq_sym_equiv]; left; split; try easy.
+Qed.
 
-(** Compatibility with compound properties. *)
+Lemma symlexT_str_conn :
+  strongly_connected R -> forall n, strongly_connected (@symlexT _ R n).
+Proof. intros; apply str_conn_conv, lexT_str_conn; easy. Qed.
 
-(* FIXME
-Lemma lex_strict_partial_order :
-  strict_partial_order R -> forall n, strict_partial_order (@lex _ R n).
+Lemma revlexT_str_conn :
+  strongly_connected R -> forall n, strongly_connected (@revlexT _ R n).
+Proof. intros; apply str_conn_conv, colexT_str_conn; easy. Qed.
+
+(** Compatibility results with compound properties. *)
+
+(** With partial order. *)
+
+Lemma lexT_partial_order :
+  partial_order R -> forall n, partial_order (@lexT _ R n).
 Proof.
-intros H n; move: H; rewrite !strict_partial_order_equiv_no_asym.
-apply modus_ponens_and; intros H; [apply lex_irrefl | apply lex_trans]; easy.
+intros H n; split; [| split]; [apply lexT_refl | apply lexT_antisym, H |].
+apply lex_trans; [left |]; apply H.
 Qed.
 
-Lemma colex_strict_partial_order :
-  strict_partial_order R -> forall n, strict_partial_order (@colex _ R n).
+Lemma colexT_partial_order :
+  partial_order R -> forall n, partial_order (@colexT _ R n).
 Proof.
-intros H n; move: H; rewrite !strict_partial_order_equiv_no_asym.
-apply modus_ponens_and; intros H;
-    [apply colex_irrefl | apply colex_trans]; easy.
+intros H n; split; [| split]; [apply colexT_refl | apply colexT_antisym, H |].
+apply colex_trans; [left |]; apply H.
 Qed.
 
-Lemma symlex_strict_partial_order :
-  strict_partial_order R -> forall n, strict_partial_order (@symlex _ R n).
+Lemma symlexT_partial_order :
+  partial_order R -> forall n, partial_order (@symlexT _ R n).
+Proof. intros; apply partial_order_conv, lexT_partial_order; easy. Qed.
+
+Lemma revlexT_partial_order :
+  partial_order R -> forall n, partial_order (@revlexT _ R n).
+Proof. intros; apply partial_order_conv, colexT_partial_order; easy. Qed.
+
+(** With total order. *)
+
+Lemma lexT_total_order : total_order R -> forall n, total_order (@lexT _ R n).
 Proof.
-intros H n; apply strict_partial_order_conv, lex_strict_partial_order; easy.
+intros H n; split; [| split; [| split]];
+    [apply lexT_refl | apply lexT_antisym, H | | apply lexT_str_conn, H].
+apply lex_trans; [left |]; apply H.
 Qed.
 
-Lemma revlex_strict_partial_order :
-  strict_partial_order R -> forall n, strict_partial_order (@revlex _ R n).
+Lemma colexT_total_order :
+  total_order R -> forall n, total_order (@colexT _ R n).
 Proof.
-intros H n; apply strict_partial_order_conv, colex_strict_partial_order; easy.
+intros H n; split; [| split; [| split]];
+    [apply colexT_refl | apply colexT_antisym, H | | apply colexT_str_conn, H].
+apply colex_trans; [left |]; apply H.
 Qed.
 
-Lemma lex_strict_total_order :
-  strict_total_order R -> forall n, strict_total_order (@lex _ R n).
+Lemma symlexT_total_order :
+  total_order R -> forall n, total_order (@symlexT _ R n).
+Proof. intros; apply total_order_conv, lexT_total_order; easy. Qed.
+
+Lemma revlexT_total_order :
+  total_order R -> forall n, total_order (@revlexT _ R n).
+Proof. intros; apply total_order_conv, colexT_total_order; easy. Qed.
+
+(** With strict partial order. *)
+
+Lemma lexF_strict_partial_order :
+  strict_partial_order R -> forall n, strict_partial_order (@lexF _ R n).
 Proof.
-intros H n; move: H; rewrite !strict_total_order_equiv_spo.
-apply modus_ponens_and; intros H;
-    [apply lex_strict_partial_order | apply lex_conn]; easy.
+intros H n; split; [| split]; [apply lexF_irrefl | apply lexF_asym, H |].
+apply lex_trans; [right |]; apply H.
 Qed.
 
-Lemma colex_strict_total_order :
-  strict_total_order R -> forall n, strict_total_order (@colex _ R n).
+Lemma colexF_strict_partial_order :
+  strict_partial_order R -> forall n, strict_partial_order (@colexF _ R n).
 Proof.
-intros H n; move: H; rewrite !strict_total_order_equiv_spo.
-apply modus_ponens_and; intros H;
-    [apply colex_strict_partial_order | apply colex_conn]; easy.
+intros H n; split; [| split]; [apply colexF_irrefl | apply colexF_asym, H |].
+apply colex_trans; [right |]; apply H.
 Qed.
 
-Lemma symlex_strict_total_order :
-  strict_total_order R -> forall n, strict_total_order (@symlex _ R n).
+Lemma symlexF_strict_partial_order :
+  strict_partial_order R -> forall n, strict_partial_order (@symlexF _ R n).
 Proof.
-intros H n; apply strict_total_order_conv, lex_strict_total_order; easy.
+intros; apply strict_partial_order_conv, lexF_strict_partial_order; easy.
 Qed.
 
-Lemma revlex_strict_total_order :
-  strict_total_order R -> forall n, strict_total_order (@revlex _ R n).
+Lemma revlexF_strict_partial_order :
+  strict_partial_order R -> forall n, strict_partial_order (@revlexF _ R n).
 Proof.
-intros H n; apply strict_total_order_conv, colex_strict_total_order; easy.
+intros; apply strict_partial_order_conv, colexF_strict_partial_order; easy.
+Qed.
+
+(** With strict total order. *)
+
+Lemma lexF_strict_total_order :
+  strict_total_order R -> forall n, strict_total_order (@lexF _ R n).
+Proof.
+intros H n; split; [| split; [| split]];
+    [apply lexF_irrefl | apply lexF_asym, H | | apply lexF_conn, H].
+apply lex_trans; [right |]; apply H.
+Qed.
+
+Lemma colexF_strict_total_order :
+  strict_total_order R -> forall n, strict_total_order (@colexF _ R n).
+Proof.
+intros H n; split; [| split; [| split]];
+    [apply colexF_irrefl | apply colexF_asym, H | | apply colexF_conn, H].
+apply colex_trans; [right |]; apply H.
+Qed.
+
+Lemma symlexF_strict_total_order :
+  strict_total_order R -> forall n, strict_total_order (@symlexF _ R n).
+Proof.
+intros; apply strict_total_order_conv, lexF_strict_total_order; easy.
+Qed.
+
+Lemma revlexF_strict_total_order :
+  strict_total_order R -> forall n, strict_total_order (@revlexF _ R n).
+Proof.
+intros; apply strict_total_order_conv, colexF_strict_total_order; easy.
 Qed.
-*)
 
-End Lex_order_Facts.
+End Lex_orders_Facts.