proposition: Lemma head_lt : forall a a' n n' b b', a < a' -> b < AP._phi0 a' -> mult_Sn (AP._phi0 a) n + b < mult_Sn (AP._phi0 a') n' + b'.
proof: Proof. intros. apply lt_le_trans with (AP._phi0 a'). - apply phi0_mult_plus_lt_phi0;auto. - apply le_trans with (mult_Sn (AP._phi0 a') n'). + induction n';simpl;auto. * left; auto. * apply le_plus_r;auto with schutte. + apply le_plus_l;auto with schutte. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)