proposition: Lemma add_comm (a b : mynat) : a + b = b + a.
proof: Proof. induction b. rewrite add_zero. rewrite zero_add. reflexivity. rewrite add_succ. rewrite IHb. rewrite succ_add. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add