proposition: Theorem add_right_cancel_iff (t a b : mynat) : a + t = b + t ↔ a = b.
proof: Proof. split. apply add_right_cancel. intro f. induction t. repeat rewrite add_zero. exact f. repeat rewrite add_succ. rewrite IHt. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid