proposition: Theorem le_succ (a b : mynat) : a ≤ b → a ≤ (succ b).
proof: Proof. intro f. destruct f as [c g]. exists (succ c). rewrite add_succ. rewrite succ_eq_succ_iff. exact g. 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