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