one_lt_div_of_mem_properDivisors — Mathlib

English

If m is a proper divisor of n, then the quotient n/m is strictly greater than 1.

Русский

Если m является собственным делителем n, то частное n/m строго больше единицы.

LaTeX

$$$ m \mid n \wedge m \neq 1 \wedge m \neq n \Rightarrow 1 < \dfrac{n}{m}$$$

Lean4

theorem one_lt_div_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) : 1 < n / m :=
  by
  obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
  rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]

Похожие утверждения