proposition: Lemma T3eq_le m n : (m == n) = ((m <= n) && (n <= m)).
proof: Proof. rewrite /T3le (eq_sym n m);case eqmn: (m == n) => //=. by case lt1: (m < n) => //; rewrite (T3lt_anti lt1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)