proposition: Theorem mul_eq_zero_iff (a b : mynat): a * b = 0 ↔ a = 0 ∨ b = 0.
proof: Proof. split. exact (eq_zero_or_eq_zero_of_mul_eq_zero a b). intro f. destruct f as [f|g]. rewrite f. exact (zero_mul b). rewrite g. exact (mul_zero a). Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition Game.World.Multiplication Game.World.Proposition Game.World.AdvancedProposition Game.World.AdvancedAddition