proposition: Lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b.
proof: Proof. induction a. rewrite mul_zero. repeat rewrite zero_add. reflexivity. rewrite succ_add. repeat rewrite mul_succ. rewrite IHa. rewrite add_right_comm. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition