Tutorial on Coercions

How to define coercions is a regularly asked questions, see for instance 
[#Rocq users > How do I code this (simple?) coercion?](https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/How.20do.20I.20code.20this.20.28simple.3F.29.20coercion.3F/with/526999320)