proposition: Lemma 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.
proof: Proof. intro x; case_eq (classify x); [|now case x..]. now rewrite (Fneg_correct radix). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig