proposition: Lemma phi0_mult_lt_phi0 (alpha beta : Ord) : alpha < beta -> forall n, (AP._phi0 alpha) * S n < AP._phi0 beta.
proof: Proof. induction n;simpl;auto. - apply phi0_mono;auto. - apply AP_plus_closed; trivial. + apply AP_phi0. + apply phi0_mono;auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)