proposition: Lemma T3add_eq0 m n: (m + n == zero) = (m == zero) && (n == zero).
proof: Proof. case: m; [by rewrite T3add0n | move => a' b' c' n' d'; rewrite andFb]. by case: n => // a b c n d /=; case: (T3ltgtP [a', b', c'] [a, b, c]). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)