proposition: Lemma coeff_lt : forall a n n' b b', b < AP._phi0 a ->(n < n')%nat -> mult_Sn (AP._phi0 a) n + b < mult_Sn (AP._phi0 a) n' + b'.
proof: Proof. intros; apply lt_le_trans with (mult_Sn (AP._phi0 a) n'). - apply lt_le_trans with (mult_Sn (AP._phi0 a) n + AP._phi0 a). + apply plus_mono_r; auto. + apply mult_Sn_mono3; auto. * apply phi0_positive; auto. - apply le_plus_l. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)