Theorem: foldFinCastLT (Controlbits/FoldFin.lean)

State before:
m : ℕ
i : Fin m
⊢ foldFin m (i.castLT ⋯) = i.castSucc
Tactic:
rw [Fin.ext_iff, coe_foldFinLT i.isLt, Fin.coe_castLT, Fin.coe_castSucc]
State after:
no goals