English
For all m, n ∈ Nat, n ∈ properDivisors(m) if and only if n ∣ m and n < m.
Русский
Для всех m, n ∈ Nat, n ∈ properDivisors(m) тогда и только тогда, когда n ∣ m и n < m.
LaTeX
$$$\forall m\in\mathbb{N},\ \ n \in \mathrm{properDivisors}(m) \iff n \mid m \land n < m$$$
Lean4
@[simp]
theorem mem_properDivisors {m : ℕ} : n ∈ properDivisors m ↔ n ∣ m ∧ n < m :=
by
rcases eq_or_ne m 0 with (rfl | hm); · simp [properDivisors]
simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]