Theorem: Nat.pair_succ_right (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
x y : Nat
⊢ x.pair (y + 1) = (x + y).tri + (x + y) + 1 + x
Tactic:
rfl
State after:
no goals

State before:
x y : Nat
⊢ (x + y).tri + (x + y) + 1 + x = (x + y).tri + (x + y) + x + 1
Tactic:
rw [Nat.add_right_comm _ x 1]
State after:
no goals

State before:
x y : Nat
⊢ (x + y).tri + (x + y) + x + 1 = (x + y).tri + x + (x + y) + 1
Tactic:
rw [Nat.add_right_comm _ (x+y) x]
State after:
no goals