proposition: Lemma T1le_trans b a c: a <= b -> b <= c -> a <= c.
proof: Proof. case /orP; first by move /eqP => ->. by move => l1 l2; rewrite /T1le (T1lt_le_trans l1 l2) orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)