no goals
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]