Missing Fin to UInt coercions

Stream: lean4

[Francisco Giordano]

I'd expect these coercions to come by default with Lean. Is there a reason why they shouldn't?

instance : Coe (Fin UInt8.size) UInt8 := ⟨UInt8.mk⟩
instance : Coe (Fin UInt16.size) UInt16 := ⟨UInt16.mk⟩
-- etc