proposition: Lemma Goodstein_decrease : forall N0 c N' c', (N0,c) -G-> (N',c') -> c = zero /\ c'=zero \/ c' < c.
proof: Proof. inversion 1. subst c0;apply goodstein_next_ord_lt. Qed.
imports: More_nat Arith ArithRing EPSILON0 Relations