coe_sub — Mathlib

English

If q ≤ p in the nonnegative rationals, then the coercion of p−q equals p−q in the rationals.

Русский

Если q ≤ p в ℚ≥0, то приведение p−q равно p−q в ℚ.

LaTeX

$$$$ q \le p \implies \big((p - q : \mathbb{Q}_{\ge 0}) : \mathbb{Q}\big) = p - q. $$$$

Lean4

@[simp, norm_cast]
theorem coe_sub (h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q :=
  max_eq_left <|
    le_sub_comm.2 <| by
      rwa [sub_zero]
        -- See note [specialised high priority simp lemma]

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