proposition: Lemma case_lt : alpha + beta = beta.
proof: Proof. unfold alpha, beta. rewrite <- (plus_assoc (mult_Sn (AP._phi0 a) n) b (mult_Sn (AP._phi0 c) p + d)). assert (b < AP._phi0 c). { apply lt_trans with (AP._phi0 a); auto with schutte. now apply phi0_mono. } rewrite (plus_assoc b (mult_Sn (AP._phi0 c) p) d). rewrite (plus_alpha_mult_phi0 _ _ H p). rewrite plus_assoc . rewrite plus_alpha_mult_phi0. auto. apply AP_mult_Sn_closed. apply AP_phi0. now apply phi0_mono. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)