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