m n : ℕ+
⊢ mod n m = m → m ≤ n
m n : ℕ+
⊢ m ∣ n → m ≤ n
rw [dvd_iff']
m n : ℕ+
h : mod n m = m
⊢ m ≤ n
m n : ℕ+
⊢ mod n m = m → m ≤ n
intro h
m n : ℕ+
h : mod n m = m
⊢ mod n m ≤ n
m n : ℕ+
h : mod n m = m
⊢ m ≤ n
rw [← h]
no goals
m n : ℕ+
h : mod n m = m
⊢ mod n m ≤ n
apply (mod_le n m).left