Theorems · Theorem · number theory
Nat.ModEq.le_of_lt_add
∀ {m a b : ℕ}, a ≡ b [MOD m] → a < b + m → a ≤ b- Defined in
- Mathlib.Data.Nat.ModEq
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- le_totalproof · cited by 294
- Nat.ModEqstatement and proof · cited by 225
- Nat.ModEq.symmproof · cited by 29
- Nat.modEq_iff_dvd'proof · cited by 11
Cited by1
Results whose statement or proof uses this declaration.
- Nat.ModEq.add_le_of_ltproof · cited by 0