proposition: Lemma FtoR_Rneg : forall beta m e, (FtoR beta true m e < 0)%R.
proof: Proof. intros beta m e. rewrite FtoR_split. now apply F2R_lt_0. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic