psub_eq_sub

Mathlib.Data.Nat.PSub

URI: https://scilib.ai/kg/mathlib#Nat.psub_eq_sub

English

If n ≤ m, psub m n = some (m - n).

Русский

Если n ≤ m, psub m n = some (m - n).

LaTeX

$$$$ \forall {m n}: \mathbb{N}, \ n \le m \Rightarrow psub(m,n) = \mathrm{some}(m-n). $$$$

Lean4

theorem psub_eq_sub {m n} (h : n ≤ m) : psub m n = some (m - n) :=
  psub_eq_some.2 <| Nat.sub_add_cancel h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru