push_neg  at np
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3