constructor
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n ∧ n / m < n
case left
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n

case right
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m < n