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