Theory HoArithUtils

theory HoArithUtils
  imports Main
begin

lemma general_theorem: 
  fixes P f and l :: nat
  assumes "(∀p. P p ∧ f p > l ⟶ (∃p'. P p' ∧ f p' < f p))"
  shows "(∀p. P p ⟶ (∃p'. P p' ∧ f p' ≤ l))"
proof-
  have "∀p. (n = f p) ∧ P p ⟶ (∃p'. P p' ∧ f p' ≤ l)" for n
    apply(rule Nat.nat_less_induct[where ?P = "%n. ∀p. (n = f p) ∧ P p ⟶ (∃p'. P p' ∧ f p' ≤ l)"])
    by (metis assms not_less)
  then show ?thesis by auto
qed

end