ring_nf
case zero

⊢ (∑ x in Finset.range (Nat.zero + 1), x) ^ 2 = ∑ x in Finset.range (Nat.zero + 1), x ^ 3
case zero

⊢ (∑ x in Finset.range (1 + Nat.zero), x) ^ 2 = ∑ x in Finset.range (1 + Nat.zero), x ^ 3