proposition: Lemma mule_eq0 x y : (x * y == 0) = (x == 0) || (y == 0).
proof: Proof. apply/idP/idP => [|/orP[] /eqP->]; rewrite ?(mule0, mul0e)//. by apply: contraTT => /norP[]; apply: mule_neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed