Coercions such as Nat.castCoe that go from a concrete structure such as
Nat to an arbitrary ring R should be set up as follows:
instance : CoeTail Nat R where coe := ...
instance : CoeHTCT Nat R where coe := ...
It needs to be CoeTail instead of Coe because otherwise type-class
inference would loop when constructing the transitive coercion Nat → Nat → Nat → ....
Sometimes we also need to declare the CoeHTCT instance
if we need to shadow another coercion
(e.g. Nat.cast should be used over Int.ofNat).