proposition: Lemma FtoR_sub : forall beta s m1 m2 e, (Zpos m2 < Zpos m1)%Z -> (FtoR beta s m1 e + FtoR beta (negb s) m2 e)%R = FtoR beta s (m1 - m2) e.
proof: Proof. intros beta s m1 m2 e Hm. rewrite 3!FtoR_split. unfold F2R. simpl. rewrite <- Rmult_plus_distr_r. rewrite <- plus_IZR. case s ; simpl. rewrite (Z.pos_sub_spec m2 m1). unfold Z.lt in Hm ; simpl in Hm. now rewrite Hm. generalize (Z.lt_gt _ _ Hm). unfold Z.gt. simpl. intros H. now rewrite (Z.pos_sub_spec m1 m2), H. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic