proposition: Lemma add_mul (a b t : mynat) : (a + b) * t = a * t + b * t.
proof: Proof. induction t. repeat rewrite mul_zero. reflexivity. repeat rewrite mul_succ. rewrite IHt. rewrite <- add_assoc. rewrite <- add_assoc. rewrite (add_right_comm _ _ a). reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition