(def-theorem 1stnsquares 
    "forall(n:zz,
          0<=n implies 
          sum(0,n,lambda(j:zz,j^2))=n*(n+1)*((2*n+1)/6))"
    (theory h-o-real-arithmetic)
    (proof
      (
    
        (cut-with-single-formula "lambda(j:zz,j^2)==delta(lambda(n:zz,(n-1)*n*((2*n-1)/6)))")
        (backchain "with(a,b:[zz,rr], a==b)")
        (apply-macete-with-minor-premises tr%telescoping-prod-formula)
        simplify
        (unfold-single-defined-constant (0) rr%delta)
        simplify
        )))