proposition: Lemma lt_aux_two (a b : mynat) : succ a ≤ b → a ≤ b ∧ ¬ (b ≤ a).
proof: Proof. intro f. split. destruct f as [c f]. exists (1 + c). rewrite <- add_assoc. exact f. intro g. pose (h := le_trans (succ a) b a f g). exact (not_succ_le_self a h). 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