proposition: Lemma FtoR_shift : forall beta s m e p, FtoR beta s m (e + Zpos p) = FtoR beta s (shift beta m p) e.
proof: Proof. intros beta s m e p. rewrite 2!FtoR_split. rewrite shift_correct. rewrite F2R_change_exp with (e' := e). ring_simplify (e + Zpos p - e)%Z. case s ; unfold cond_Zopp. now rewrite Zopp_mult_distr_l_reverse. apply refl_equal. pattern e at 1 ; rewrite <- Zplus_0_r. now apply Zplus_le_compat_l. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic