proposition: Lemma phi0_mult_plus_lt_phi0R alpha beta n gamma : mult_Sn (AP._phi0 alpha) n + beta < AP._phi0 gamma -> alpha < gamma /\ beta < AP._phi0 gamma.
proof: Proof. split. - assert (H0 : AP._phi0 alpha < AP._phi0 gamma). { eapply le_lt_trans. 2:eexact H. apply le_trans with (mult_Sn (AP._phi0 alpha) n). clear H; induction n. simpl;auto with schutte. simpl; apply le_plus_r. apply le_plus_l;auto with schutte. } apply phi0_mono_R;auto. - eapply le_lt_trans. 2:eexact H. apply le_plus_r;auto with schutte. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)