proposition: Lemma toX_Float : forall m e, toX (Float m e) = Xreal (toR (Float m e)).
proof: Proof. intros m e. unfold toR, toX, toF. now destruct mantissa_sign. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig