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