Modular induction

Stream: new members

[Jeremy Tan]

What's the cleanest way to set up "modular induction" as below?

@[elab_as_elim]
theorem mod_induction (hk : 0 < k) {P : Nat → Prop} (base : ∀ n < k, P n)
    (succ : ∀ n, P n → P (n + k)) : ∀ n, P n := by
  sorry

[Yaël Dillies]

docs#Nat.mod.inductionOn

[Jeremy Tan]

Yes, but it looks unwieldy to use

[Yaël Dillies]

Sure but probably you can start from there

[Yaël Dillies]

... or at least get inspiration from the proof