proposition: Lemma T1mul_eq0 x y: (x * y == zero) = (x== zero) || (y == zero).
proof: Proof. case: y x => [ [] |a n b] // [] // a' n' b' /=. by case : (_ && _) => //; case: (a==zero). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)