proposition: Theorem le_total (a b : mynat) : a ≤ b ∨ b ≤ a.
proof: Proof. induction a. left. exact (zero_le b). destruct IHa as [f|g]. destruct f as [c f]. destruct c. right. exists 1. rewrite f. reflexivity. left. rewrite f. exists c. rewrite add_succ. rewrite succ_add. reflexivity. right. apply le_succ. 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