proposition: Lemma T1leNgt a b: (a <= b) = ~~ (b < a).
proof: Proof. case /or3P: (T1lt_trichotomy a b). - by move => h; rewrite (T1lt_anti h) (T1ltW h). - by move /eqP ->; rewrite T1ltnn T1lenn. - by move => h; rewrite h /T1le (T1lt_anti h) (T1lt_ne' h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)