proposition: Lemma T1lt_le_trans b a c: a < b -> b <= c -> a < c.
proof: Proof. by move => lab; case /orP;[ move /eqP => <- | apply:T1lt_trans]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)