proposition: Lemma lt_aux_one (a b : mynat) : a ≤ b ∧ ¬ (b ≤ a) → succ a ≤ b.
proof: Proof. intro f. destruct f as [f g]. destruct f as [c f]. destruct c. exfalso. apply g. exists 0. rewrite f. reflexivity. exists c. rewrite succ_add. rewrite add_succ in f. 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