proposition: Lemma FtoR_split : forall beta s m e, FtoR beta s m e = F2R (Defs.Float beta (cond_Zopp s (Zpos m)) e).
proof: Proof. intros. unfold FtoR, F2R, cond_Zopp. simpl. case e. now rewrite Rmult_1_r. intros p. now rewrite mult_IZR. now intros p. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal