case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun x => x ∣ n) (range n) ↔ a✝ ∈ properDivisors n
n : ℕ
h : n ≠ 0
⊢ filter (fun x => x ∣ n) (range n) = properDivisors n
ext
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n → 1 ≤ a✝
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun x => x ∣ n) (range n) ↔ a✝ ∈ properDivisors n
simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
no goals
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n → 1 ≤ a✝
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)