Theorems · Theorem · number theory
PNat.add_sub_of_lt
∀ {a b : ℕ+}, a < b → a + (b - a) = b- Defined in
- Mathlib.Data.PNat.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LT.lt.leproof · cited by 2,189
- PNatstatement and proof · cited by 392
- PNat.valproof · cited by 226
- add_tsub_cancel_of_leproof · cited by 79
- PNat.eqproof · cited by 9
- PNat.sub_coeproof · cited by 3
- PNat.add_coeproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- PNat.sub_add_of_ltproof · cited by 1