FPCore.fprec_lt_femax should be via (Pos2Z.is_pos (fprecp _))

[andrew-appel]

In order to avoid extra (annoying) uses of proof irrelevance, especially when unfolding Zconst, then either

1. The proof of FPCore.fprec_lt_femax should just be (Pos2Z.is_pos (fprecp _)), transparently (Defined, not Qed); or
2. The definition of Zconst should use FPCore.fprec_lt_femax;

or both (1) and (2).