onModCases_succ

Mathlib.Tactic.ModCases

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

Lean4

/-- The successor case decomposes `∃ z, b ≤ z < n ∧ a ≡ z (mod n)` into
`a ≡ b (mod n) ∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n)`,
and the `a ≡ b (mod n) → p` case becomes a subgoal.
-/
@[inline]
def onModCases_succ {p : Sort*} {n : ℕ} {a : ℤ} (b : ℕ) (h : a ≡ OfNat.ofNat b [ZMOD OfNat.ofNat 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