proposition: Lemma one_mul (a : mynat) : 1 * a = a .
proof: Proof. induction a. reflexivity. rewrite mul_succ. rewrite IHa. rewrite succ_eq_add_one. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition