proposition: Lemma T2ltgtP m n : compare_T2 m n (m < n) (n < m) (m == n).
proof: Proof. rewrite T2lt_neAle T2eq_le;case: T2ltP; first by constructor. by rewrite T2le_eqVlt orbC; case: T2leP; constructor; first exact /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)