onModCases_start

Mathlib.Tactic.ModCases

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

Lean4

/-- The first theorem we apply says that `∃ m, 0 ≤ m < n ∧ a ≡ m (mod n)`.
The actual mathematical content of the proof is here.
-/
@[inline]
def onModCases_start (p : Sort _) (a : ℕ) (n : ℕ) (hn : Nat.ble 1 n = true) (H : OnModCases n a (nat_lit 0) p) : p :=
  H (a % n) <| by
    refine ⟨Nat.zero_le _, ?_, ?_⟩
    · exact Nat.mod_lt _ (Nat.le_of_ble_eq_true hn)
    · rw [Nat.ModEq, Nat.mod_mod]

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

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

Разделы

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

Аффилиация

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