instOrderedSub — Mathlib

English

ℕ has an ordered subtraction structure: for m ≤ n, there exists k with m + k = n.

Русский

ℕ имеет упорядоченную операцию вычитания: для m ≤ n существует k с m + k = n.

LaTeX

$$$m \le n \Rightarrow \exists k\, (m+k=n).$$$

Lean4

instance instOrderedSub : OrderedSub ℕ := by
  refine ⟨fun m n k ↦ ?_⟩
  induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

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