proposition: Lemma T1lt_trichotomy a b: [|| (a< b), (a==b) | (b < a)].
proof: Proof. elim: a b; first by case; [rewrite eqxx // | move => a n b]. move => a Ha n b Hb [] // a' n' b' /=. case /or3P: (Ha a'); [by move => -> | | by move => ->; rewrite !orbT ]. move => h; rewrite h (eqP h) T1ltnn eqxx. case : (ltngtP n n'); [done | by rewrite !orbT | move => -> ]. by rewrite T1eqE !eqxx /= Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)