Cofactor lemma in Lean: if d ∈ properDivisors n and n/3 < d then d = n/2

Result

Let $n,d\in\mathbb N$. If $d$ is a proper divisor of $n$ and $\frac n3<d$, then $d=\frac n2$.

Equivalently: among proper divisors of $n$, the only one strictly larger than $n/3$ is the largest proper divisor $n/2$.

This lemma is a reusable cofactor trick and can be used to identify the second-largest proper divisor in divisor-ordering arguments.

Lean4 / mathlib formalization

import Mathlib.NumberTheory.Divisors

namespace Math.DivisorSequence

/-- Cofactor trick for `k=3`: a proper divisor strictly greater than `n/3` must be `n/2`.

More precisely, if `d ∈ n.properDivisors` and `n/3 < d`, then `d = n/2`.
-/
theorem eq_div_two_of_mem_properDivisors_of_div_three_lt {n d : ℕ}
    (hd : d ∈ n.properDivisors) (h : n / 3 < d) : d = n / 2 := by
  classical
  have hn0 : n ≠ 0 := by
    intro hn0
    subst hn0
    simpa [Nat.properDivisors_zero] using hd
  -- write `n = d*k` with `k>1`
  rcases (Nat.mem_properDivisors_iff_exists (m := d) (n := n) hn0).1 hd with ⟨k, hk, hnk⟩
  -- from `n/3 < d` deduce `n < d*3`
  have hmul : n < d * 3 := (Nat.div_lt_iff_lt_mul (by decide : 0 < 3)).1 h
  -- rewrite as `d*k < d*3` and cancel
  have hmul' : d * k < d * 3 := by
    simpa [hnk, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using hmul
  have hklt3 : k < 3 := Nat.lt_of_mul_lt_mul_left hmul'
  have hk_le2 : k ≤ 2 := (Nat.lt_succ_iff).1 (by simpa using hklt3)
  have hk_ge2 : 2 ≤ k := (Nat.succ_le_iff).2 hk
  have hk2 : k = 2 := le_antisymm hk_le2 hk_ge2
  -- from `n=d*2`, `n/2 = d`
  have : n / 2 = d := by
    simpa [hnk, hk2, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using
      (Nat.mul_div_right d 2)
  simpa [this]

end Math.DivisorSequence

Compilation output

$ cd /opt/lean/Math
$ lake env lean Math/DivisorSequence/Cofactor.lean
# success (only minor linter warnings)