m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (¬∃ m, m < n + 1 ∧ P m) ↔ ¬((∃ m, m < n ∧ P m) ∨ P n)
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P n
rw [← not_iff_not]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 → ¬P m) ↔ (∀ (m : ℕ), m < n → ¬P m) ∧ ¬P n
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (¬∃ m, m < n + 1 ∧ P m) ↔ ¬((∃ m, m < n ∧ P m) ∨ P n)
push_neg
no goals
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 → ¬P m) ↔ (∀ (m : ℕ), m < n → ¬P m) ∧ ¬P n
exact forall_lt_succ