feat: make Fin.foldl reduce in the kernel (#14267)

This PR makes `Fin.foldl` reduce in the kernel by marking its inner
`loop` `semireducible` (well-founded definitions are `irreducible` by
default) and exposing `foldl`, so the kernel's special support for
well-founded recursion on `Nat` applies. Previously `Fin.foldl` got
stuck under `decide`/`#reduce`/`Decidable`, unlike the already-reducing
`Fin.foldr`:

```lean
example : Fin.foldl 8 (fun a i => a + i.val) 0 = 28 := by decide  -- now succeeds
```

The definition and all lemmas are unchanged.