proposition: Lemma FtoR_add : forall beta s m1 m2 e, (FtoR beta s m1 e + FtoR beta s m2 e)%R = FtoR beta s (m1 + m2) e.
proof: Proof. intros beta s m1 m2 e. rewrite 3!FtoR_split. unfold F2R. simpl. rewrite <- Rmult_plus_distr_r. rewrite <- plus_IZR. now case s. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic