proposition: Theorem succ_succ_inj {a b : mynat} (h : succ(succ(a)) = succ(succ(b))): a = b.
proof: Proof. apply succ_inj. apply succ_inj. exact h. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid