proposition: Lemma leqif_trans m1 m2 m3 C12 C23 : m1 <= m2 ?= iff C12 -> m2 <= m3 ?= iff C23 -> m1 <= m3 ?= iff C12 && C23.
proof: Proof. move=> ltm12 ltm23; apply/leqifP; rewrite -ltm12. have [->|eqm12] := eqVneq; first by rewrite ltn_neqAle !ltm23 andbT; case C23. by rewrite (@leq_trans m2) ?ltm23 // ltn_neqAle eqm12 ltm12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring