proposition: Theorem not_succ_le_self (a : mynat) : ¬ (succ a ≤ a).
proof: Proof. intro f. pose (g := le_antisymm a (succ a) (le_succ_self a)). apply g in f. apply (ne_succ_self a). exact f. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Le Game.World.Addition Game.World.Multiplication Game.World.Proposition Game.World.AdvancedProposition Game.World.AdvancedAddition Game.World.AdvancedMultiplication