proposition: Lemma muln_eq0 m n : (m * n == 0) = (m == 0) || (n == 0).
proof: Proof. case: m => [|p]. by []. case: n => [|k]; last first. by []. Abort. Search _ (_ * 0) inside ssrnat. Search _ muln 0 inside ssrnat. Print right_zero. Search right_zero. Lemma muln_eq0 m n : (m * n == 0) = (m == 0) || (n == 0). Proof. case: m => [|p]. by []. case: n => [|q]. rewrite muln0. by []. by []. Qed.
imports: mathcomp(all_ssreflect)