p : ℕ
⊢ Nat.rec 0 (fun y IH => (unpair p).fst + IH) (unpair p).snd = (unpair p).fst * (unpair p).snd
p : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec 0
          (fun y IH =>
            unpaired (fun x x_1 => x + x_1)
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).fst
                (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 0 (fun y IH => (unpair p).fst + IH) (unpair p).snd = (unpair p).fst * (unpair p).snd
induction p.unpair.2 <;> simp [*, mul_succ, add_comm _ (unpair p).fst]