Classical Logic with Cut rule: using Stolzengerg Principle, prove that that every f:N→N has three 0's or  three non-0's.
A Cut between Stolzenberg and
(Stolzenberg
→
( ∃x.∃y.∃z.((x<y∧y<z)∧(f(x)=0∧(f(y)=0∧f(z)=0)))
  ∨
  ∃x.∃y.∃z.((x<y∧y<z)∧(f(x)>0∧(f(y)>0∧f(z)>0)))))