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

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

State before:
y : Nat
⊢ (0 + y).tri = y.tri
Tactic:
rw [Nat.zero_add]
State after:
no goals