Theorem: C05S03.aux (LeanCourse/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n ∧ n / m < n
Tactic:
sorry
State after:
no goals