proposition: Lemma mul_one (a : mynat) : a * 1 = a.
proof: Proof. rewrite one_eq_succ_zero. rewrite mul_succ. rewrite mul_zero. rewrite zero_add. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition