proposition: Lemma T3le_total m n : (m <= n) || (n <= m).
proof: Proof. by rewrite /T3le;case /or3P: (T3lt_trichotomy m n) => -> //; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)