proposition: Lemma neg_correct : forall x, match classify x with | Freal => toX (neg x) = Xneg (toX x) | Sig.Fnan => classify (neg x) = Sig.Fnan | Fminfty => classify (neg x) = Fpinfty | Fpinfty => classify (neg x) = Fminfty end.
proof: Proof. intro x. case_eq (classify x); [|now case x..]. intro Cx. destruct x as [| m e]. apply refl_equal. unfold toX. simpl. generalize (mantissa_sign_correct m). case_eq (mantissa_sign m). simpl. intros -> _. now rewrite Ropp_0. intros s p H0 [H1 H2]. generalize (toF_float (negb s) p e H2). destruct s ; simpl ; intros -> ; now rewrite FtoR_neg. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig