proposition: Lemma leif_trans x1 x2 x3 C12 C23 : x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23.
proof: Proof. move=> ltx12 ltx23; apply/leifP; rewrite -ltx12. case eqx12: (x1 == x2). by rewrite (eqP eqx12) lt_neqAle !ltx23 andbT; case C23. by rewrite (@lt_le_trans x2) ?ltx23 // lt_neqAle eqx12 ltx12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)