proposition: Lemma succ_mul (a b : mynat) : succ a * b = a * b + b.
proof: Proof. induction b. repeat rewrite mul_zero. reflexivity. repeat rewrite mul_succ. rewrite IHb. repeat rewrite add_succ. rewrite add_right_comm. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition