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