proposition: Lemma add_left_eq_zero {a b : mynat} (H : a + b = 0) : b = 0.
proof: Proof. destruct b. reflexivity. exfalso. apply (succ_ne_zero (a + b)). rewrite add_succ in H. exact H. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid