Get rid of Z.of_nat coercion
Coercions, in the long run, often turn out to cause more confusion that they are worth, so we have gotten rid of a bunch of them in Iris recently -- and I propose we also get rid of the number type coercions Z.of_nat
(and Qc_of_Z
-- this latter part is done). The former makes many goals basically impossible to prove until one does Set Printing Coercions
to see what is really going on.