FPStdLib.fprec_gt_one <> FPCore.fprec_gt_one

[andrew-appel]

These two opaque proofs are not equal: FPStdLib.fprec_gt_one , FPCore.fprec_gt_one
Consequently, the following two expressions are not convertible,

Binary.Bfma (fprec Tdouble) (femax Tdouble)
  (fprec_gt_0 Tdouble) (fprec_lt_femax Tdouble)
  (FPCore.fma_nan (fprec Tdouble)
     (femax Tdouble) (fprec_gt_one Tdouble))
  BinarySingleNaN.mode_NE

Binary.Bfma (FPCore.fprec FPCore.Tdouble) 1024
  (FPCore.fprec_gt_0 FPCore.Tdouble)
  (FPCore.fprec_lt_femax FPCore.Tdouble)
  (FPCompCert.FMA_NAN.fma_nan_pl
     (FPCore.fprec FPCore.Tdouble) 1024
     (FPCore.fprec_gt_one FPCore.Tdouble))
  BinarySingleNaN.mode_NE

which is quite inconvenient.
One of these two proofs should be defined as the other.