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