proposition: Lemma sqrt_error_N_FLX_aux1 x (Fx : format x) (Px : (0 < x)%R) : exists (mu : R) (e : Z), (format mu /\ x = mu * bpow (2 * e) :> R /\ 1 <= mu < bpow 2)%R.
proof: Proof. set (e := ((mag beta x - 1) / 2)%Z). set (mu := (x * bpow (-2 * e)%Z)%R). assert (Hbe : (bpow (-2 * e) * bpow (2 * e) = 1)%R). { now rewrite <- bpow_plus; case e; simpl; [reflexivity| |]; intro p; rewrite Z.pos_sub_diag. } assert (Fmu : format mu); [now apply mult_bpow_exact_FLX|]. exists mu, e; split; [exact Fmu|split; [|split]]. { set (e2 := (2 * e)%Z); simpl; unfold mu; rewrite Rmult_assoc. now unfold e2; rewrite Hbe, Rmult_1_r. } { apply (Rmult_le_reg_r (bpow (2 * e))). { apply bpow_gt_0. } rewrite Rmult_1_l; set (e2 := (2 * e)%Z); simpl; unfold mu. unfold e2; rewrite Rmult_assoc, Hbe, Rmult_1_r. apply (Rle_trans _ (bpow (mag beta x - 1))). { now apply bpow_le; unfold e; apply Z_mult_div_ge. } set (l := mag _ _); rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Px)). unfold l; apply bpow_mag_le. intro Hx; revert Px; rewrite Hx; apply Rlt_irrefl. } simpl; unfold mu; change (IZR _) with (bpow 2). apply (Rmult_lt_reg_r (bpow (2 * e))); [now apply bpow_gt_0|]. rewrite Rmult_assoc, Hbe, Rmult_1_r. apply (Rlt_le_trans _ (bpow (mag beta x))). { rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Px)) at 1; apply bpow_mag_gt. } rewrite <- bpow_plus; apply bpow_le; unfold e; set (mxm1 := (_ - 1)%Z). replace (_ * _)%Z with (2 * (mxm1 / 2) + mxm1 mod 2 - mxm1 mod 2)%Z by ring. rewrite <- Z.div_mod; [|now simpl]. apply (Zplus_le_reg_r _ _ (mxm1 mod 2 - mag beta x)%Z). unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error