Get rid of Z.of_nat and Qc_of_Z coercions
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
Qc_of_Z. The former makes many goals basically impossible to prove until one does
Set Printing Coercions to see what is really going on.