dvd_sub_self_left — Mathlib

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

Похожие утверждения