proposition: Lemma add_right_eq_zero {a b : mynat} : a + b = 0 → a = 0.
proof: Proof. intro f. rewrite add_comm in f. apply (@add_left_eq_zero b a) in f. exact f. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid