proposition: Lemma T2leNgt a b: (a <= b) = ~~ (b < a).
proof: Proof. case /or3P: (T2lt_trichotomy a b). - by move => h; rewrite (T2lt_anti h) (T2ltW h). - by move /eqP ->; rewrite T2ltnn T2lenn. - by move => h; rewrite h /T2le (T2lt_anti h) (T2lt_ne' h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)