proposition: Lemma T1ltgtP m n : compare_T1 m n (m < n) (n < m) (m == n).
proof: Proof. rewrite T1lt_neAle T1eq_le;case: T1ltP; first by constructor. by rewrite T1le_eqVlt orbC; case: T1leP; constructor; first exact /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)