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

State before:
x y : Nat
⊢ ↑(x.pair y).split.snd = x
Tactic:
apply Nat.add_left_cancel (n:=tri (split (pair x y)).fst)
State after:
x y : Nat
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x.pair y).split.fst.tri + x

State before:
x y : Nat
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x.pair y).split.fst.tri + x
Tactic:
rw [split_eq, split_pair_fst, pair]
State after:
no goals