proposition: Lemma lt_iff_succ_le (a b : mynat) : a < b ↔ succ a ≤ b.
proof: Proof. split. exact (lt_aux_one a b). exact (lt_aux_two a b). 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