onModCases_succ

Mathlib.Tactic.ModCases

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

Lean4

/-- The successor case decomposes `∃ m, b ≤ m < n ∧ a ≡ m (mod n)` into
`a ≡ b (mod n) ∨ ∃ m, b+1 ≤ m < n ∧ a ≡ m (mod n)`,
and the `a ≡ b (mod n) → p` case becomes a subgoal.
-/
@[inline]
def onModCases_succ {p : Sort _} {n : ℕ} {a : ℕ} (b : ℕ) (h : a ≡ b [MOD n] → p) (H : OnModCases n a (Nat.add b 1) p) :
    OnModCases n a b p := fun z ⟨h₁, h₂⟩ => if e : b = z then h (e ▸ h₂.2) else H _ ⟨Nat.lt_of_le_of_ne h₁ e, h₂⟩

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

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

Разделы

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

Аффилиация

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