proposition: Lemma ne_succ_self (n : mynat) : n ≠ succ n.
proof: Proof. induction n. apply zero_ne_succ. intro f. rewrite succ_eq_succ_iff in f. apply IHn. exact f. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid