p : ℕ
⊢ Nat.rec (unpair p).fst (fun y IH => Nat.pred IH) (unpair p).snd = (unpair p).fst - (unpair p).snd
p : ℕ
⊢ unpaired (fun z n => Nat.rec (id z) (fun y IH => Nat.pred (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).snd) n)
      p =
    unpaired (fun x x_1 => x - x_1) p
simp
no goals
p : ℕ
⊢ Nat.rec (unpair p).fst (fun y IH => Nat.pred IH) (unpair p).snd = (unpair p).fst - (unpair p).snd
induction p.unpair.2 <;> simp [*, sub_succ]