Theorem: coe_foldFinLE (Controlbits/FoldFin.lean)

State before:
m : ℕ
i : Fin (2 * m + 1)
h : ↑i ≤ m
⊢ ↑(foldFin m i) = ↑i
Tactic:
simp_rw [foldFin, Nat.lt_succ_of_le h, dite_true, Fin.coe_castLT]
State after:
no goals