proposition: Lemma T3ltgtP m n : compare_T3 m n (m < n) (n < m) (m == n).
proof: Proof. rewrite T3lt_neAle T3eq_le;case: T3ltP; first by constructor. by rewrite T3le_eqVlt orbC; case: T3leP; constructor; first exact /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)