English
A standard relation about n ∣ n − m: n divides n−m iff m=0 or n≤m.
Русский
Пусть n,m ∈ ℕ; тогда n | (n−m) эквивалентно (m=0) или (n ≤ m).
LaTeX
$$$\forall n,m \in \mathbb{N},\; n \mid (n- m) \iff (m=0 \lor n \le m)$$$
Lean4
@[simp]
protected theorem dvd_sub_self_left {n m : ℕ} : n ∣ n - m ↔ m = 0 ∨ n ≤ m :=
by
rcases le_or_gt n m with h | h
· simp [h]
· rcases eq_or_ne m 0 with rfl | hm
· simp
· simp only [hm, h.not_ge, or_self, iff_false]
refine not_dvd_of_pos_of_lt ?_ ?_ <;> grind