∀ (n : ℕ),
  6 * (n + 2).smallSchroder + 4 * ∑ i ∈ Finset.Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder =
    2 *
      (3 * (n + 1 + 1).smallSchroder +
        2 * ∑ i ∈ Finset.Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder)