proposition: Lemma phi0_mult_plus_lt_phi0 alpha beta n gamma : alpha < gamma -> beta < AP._phi0 gamma -> mult_Sn (AP._phi0 alpha) n + beta < AP._phi0 gamma.
proof: Proof. intros;apply AP_plus_closed ; auto with schutte. - apply AP_phi0. - apply phi0_mult_lt_phi0;auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)