proposition: Lemma cprod2_eq0 a b: a *c b = \0c -> a = \0c \/ b = \0c.
proof: Proof. move =>h. case: (equal_or_not a \0c) => az; first by left. case: (equal_or_not b \0c) => bz; first by right. by case: (cprod2_nz az bz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)