proposition: Theorem eq_zero_of_add_right_eq_self {a b : mynat} : a + b = a → b = 0.
proof: Proof. intro f. induction a. rewrite zero_add in f. exact f. rewrite add_comm in f. rewrite add_succ in f. rewrite add_comm in f. rewrite succ_eq_succ_iff in f. exact (IHa f). Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid