fact: Parameter neg_correct : forall x, match classify x with | Freal => toX (neg x) = Xneg (toX x) | Fnan => classify (neg x) = Fnan | Fminfty => classify (neg x) = Fpinfty | Fpinfty => classify (neg x) = Fminfty end.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic