proposition: Lemma goodstein_next_ord_lt : forall N0 c (H:nf c) (H0 : correct (S (S N0)) c), (c = zero /\ goodstein_next_ord N0 c H H0 = zero) \/ goodstein_next_ord N0 c H H0 < c.
proof: Proof. unfold goodstein_next_ord;intros. case (goodstein_next N0 c H H0). intros. tauto. Qed.
imports: More_nat Arith ArithRing EPSILON0