case inl
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : n ≤ m
⊢ k ∣ m - n

case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ m - n
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
⊢ k ∣ m - n
cases' le_total n m with H H
no goals
case inl
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : n ≤ m
⊢ k ∣ m - n
exact dvd_sub H h₁ h₂
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ 0
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ m - n
rw [tsub_eq_zero_iff_le.mpr H]
no goals
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ 0
exact dvd_zero k