onModCases_stop

Mathlib.Tactic.ModCases

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ModCases.NatMod.onModCases_stop

Lean4

/-- The end point is that once we have reduced to `∃ m, n ≤ m < n ∧ a ≡ m (mod n)`
there are no more cases to consider.
-/
@[inline]
def onModCases_stop (p : Sort _) (n : ℕ) (a : ℕ) : OnModCases n a n p := fun _ h => (Nat.not_lt.2 h.1 h.2.1).elim

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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