Add new Fin instances, extend the UInt declarations to other UInt types using a macro. This incorporates @gebner's suggestions to add boolean methods for checking under/overflow, and adding separate instances of `Fin size`. I still can't figure out the elaboration issue mentioned [here on zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20type.20annotations/near/260877092), so I can't use the macro on USize yet.

Switch over to using the `[Inhabited (Fin n)]` bound, inilne lemmas where possible, and add USize. The Inhabited bound is needed to deal with the combination of `USize.size` not being defined in terms of `Nat.succ`, and `Zero` not giving enough information (by itself) to prove the lemmas needed for classes like AddMonoid. We need to know that `0` from OfNat.ofNat is definitionally equal to something that actually has the requisite properties.

Inline more items to Ring/CommRing, change some names for consistency.