proposition: Lemma BtoX_Bopp x : BtoX (Bopp x) = (- (BtoX x))%XR.
proof: Proof. case x as [s|s| |s m e B]; [ |now simpl..| ]. { now simpl; rewrite Ropp_0. } now simpl; rewrite Generic_proof.FtoR_neg. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig