(lset comb-ident (qr "forall(k,m:zz, 1<=k and k<=m implies comb(1+m,k)=comb(m,k-1)+comb(m,k))")) (lset 1stnsquares (qr "forall(n:zz, 0<=n implies sum(0,n,lambda(j:zz,j^2))=n*(n+1)*(2*n+1)/6)")) (lset bernoullis-inequality (qr "forall(h:rr,n:zz,-1<h and 1<=n implies 1+n*h<=(1+h)^n)"))