proposition: Lemma mul_assoc (a b c : mynat) : (a * b) * c = a * (b * c).
proof: Proof. induction c. repeat rewrite mul_zero. reflexivity. repeat rewrite mul_succ. rewrite IHc. rewrite mul_add. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition