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.