proposition: Lemma le_zero (a : mynat) (h : a ≤ 0) : a = 0.
proof: Proof. destruct h as [c h]. symmetry in h. exact (add_right_eq_zero 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