proposition: Lemma FtoR_abs : forall beta s m e, (Rabs (FtoR beta s m e) = FtoR beta false m e)%R.
proof: Proof. intros beta s m e. rewrite 2!FtoR_split, <- F2R_abs. now case s. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic