proposition: Lemma zero_lt alpha n beta : zero < mult_Sn (AP._phi0 alpha) n + beta.
proof: Proof. apply lt_le_trans with (AP._phi0 alpha). - apply phi0_positive;auto. - apply le_trans with ( mult_Sn (AP._phi0 alpha) n). induction n; simpl; auto with schutte. + apply le_plus_r;auto. + apply le_plus_l;auto with schutte. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)