proposition: Lemma add_squared (a b : mynat) : (a + b) ^ (2 : mynat) = a ^ (2 : mynat) + b ^ (2 : mynat) + 2 * a * b.
proof: Proof. rewrite two_eq_succ_one. rewrite one_eq_succ_zero. repeat rewrite pow_succ. repeat rewrite pow_zero. repeat rewrite one_mul. rewrite succ_mul. rewrite one_mul. rewrite mul_add. repeat rewrite add_mul. rewrite add_assoc. rewrite <- (add_assoc (b * a) _ _ ). rewrite (add_comm _ (b * b)). rewrite (add_comm (b * a) _). rewrite (mul_comm b a). rewrite <- add_assoc. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Pow Game.World.Addition Game.World.Multiplication