proposition: Lemma one_add_le_self (x : mynat) : x ≤ 1 + x.
proof: Proof. rewrite le_iff_exists_add. exists 1. exact (add_comm 1 x). 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