no goals
n : ℕ
⊢ catalan (n + 1) = ∑ ij in Nat.antidiagonal n, catalan ij.fst * catalan ij.snd
rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,
  sum_range]