Theorem: IMOSL.IMO2006N3.two_le_card_divisors (IMOSLLean4/IMO2006/N3/N3.lean)

State before:
n : ℕ
h : 2 ≤ n
⊢ 2 ≤ n.divisors.card
Tactic:
rw [← Nat.insert_self_properDivisors (Nat.not_eq_zero_of_lt h), Nat.succ_le_iff,
  card_insert_of_not_mem Nat.properDivisors.not_self_mem, Nat.succ_lt_succ_iff, card_pos]
State after:
n : ℕ
h : 2 ≤ n
⊢ n.properDivisors.Nonempty

State before:
n : ℕ
h : 2 ≤ n
⊢ n.properDivisors.Nonempty
Tactic:
exact ⟨1, Nat.one_mem_properDivisors_iff_one_lt.mpr h⟩
State after:
no goals