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