proposition: Lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c).
proof: Proof. induction c. rewrite add_zero. rewrite add_zero. reflexivity. rewrite add_succ. rewrite IHc. rewrite add_succ. rewrite add_succ. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add