Lean4
/-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
there is a map from `C n` to each `C m`, `n ≤ m`.
This is a version of `Nat.le.rec` that works for `Sort u`.
Similarly to `Nat.le.rec`, it can be used as
```
induction hle using Nat.leRec with
| refl => sorry
| le_succ_of_le hle ih => sorry
```
-/
@[elab_as_elim]
def leRec {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl : motive n (Nat.le_refl _))
(le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) : ∀ {m} (h : n ≤ m), motive m h
| 0, H => Nat.eq_zero_of_le_zero H ▸ refl
| m + 1, H =>
(le_succ_iff.1 H).by_cases (fun h : n ≤ m ↦ le_succ_of_le h <| leRec refl le_succ_of_le h)
(fun h : n = m + 1 ↦ h ▸ refl)
-- This verifies the signatures of the recursor matches the builtin one, as promised in the
-- above.
