proposition: Lemma mag_plus : forall x y, (0 < y)%R -> (y <= x)%R -> (mag x <= mag (x + y) <= mag x + 1)%Z.
proof: Proof. assert (Hr : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Hy Hxy. assert (Hx : (0 < x)%R) by apply (Rlt_le_trans _ _ _ Hy Hxy). destruct (mag x) as (ex,Hex); simpl. destruct Hex as (Hex0,Hex1); [now apply Rgt_not_eq|]. assert (Haxy : (Rabs (x + y) < bpow (ex + 1))%R). { rewrite bpow_plus_1. apply Rlt_le_trans with (2 * bpow ex)%R. - rewrite Rabs_pos_eq. apply Rle_lt_trans with (2 * Rabs x)%R. + rewrite Rabs_pos_eq. replace (2 * x)%R with (x + x)%R by ring. now apply Rplus_le_compat_l. now apply Rlt_le. + apply Rmult_lt_compat_l with (2 := Hex1). exact Rlt_0_2. + rewrite <- (Rplus_0_l 0). now apply Rlt_le, Rplus_lt_compat. - apply Rmult_le_compat_r. now apply bpow_ge_0. now apply IZR_le. } assert (Haxy2 : (bpow (ex - 1) <= Rabs (x + y))%R). { apply (Rle_trans _ _ _ Hex0). rewrite Rabs_right; [|now apply Rgt_ge]. apply Rabs_ge; right. rewrite <- (Rplus_0_r x) at 1. apply Rplus_le_compat_l. now apply Rlt_le. } split. - now apply mag_ge_bpow. - apply mag_le_bpow. + now apply tech_Rplus; [apply Rlt_le|]. + exact Haxy. Qed.
imports: Coq(Psatz Reals ZArith) Zaux