fact: Definition goodstein_next N0 c (H:nf c) (H0 : correct (S (S N0)) c) : {c' : T1 | nf c' /\ correct (S (S (S N0))) c' /\ (c=zero /\ c'=zero \/ c' < c) /\ val (S (S (S N0))) c' = Peano.pred (val (S (S (S N0))) c)}.
imports: More_nat Arith ArithRing EPSILON0