proposition: Theorem succ_eq_succ_iff (a b : mynat) : succ a = succ b ↔ a = b.
proof: Proof. split. exact succ_inj. intro f. rewrite f. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid