proposition: Lemma c1_n_correct : forall x n, (/ 256 * 2^Pos.to_nat n <= Rabs (F.toR x))%R -> F.toX (iter_pos F.div2 n x) = Xmul (F.toX x) (Xreal ((/2)^Pos.to_nat n)).
proof: Proof. intros x n Hx. rewrite iter_pos_nat. revert x Hx. elim (Pos.to_nat n); clear n; [|intros n IHn]; intros x Hx. { now simpl; case F.toX; [|intro r; simpl; rewrite Rmult_1_r]. } simpl. rewrite IHn. { rewrite F.div2_correct; [|easy|]. { rewrite Xdiv_split. case F.toX; [easy|]; intro rx. simpl; unfold Xinv'; rewrite is_zero_false; [|easy]. now simpl; rewrite Rmult_assoc. } revert Hx; apply Rle_trans. unfold Rdiv; rewrite Rmult_1_l. rewrite <-(Rmult_1_r (/ 256)) at 1. apply Rmult_le_compat_l; [|apply pow_R1_Rle]; lra. } unfold F.toR; rewrite F.div2_correct; [|easy|]. { revert Hx; unfold F.toR; case F.toX; [|intro rx]. { simpl; change R0 with 0%R; rewrite Rabs_R0. intro H; exfalso; apply (Rlt_irrefl 0); revert H; apply Rlt_le_trans. do 2 (apply Rmult_lt_0_compat; [lra|]). apply pow_lt; lra. } rewrite Xdiv_split; unfold Xinv'. simpl. intro Hx. rewrite is_zero_false; [|easy]. simpl. rewrite Rabs_mult, (Rabs_pos_eq (/ 2)); lra. } revert Hx; apply Rle_trans. unfold Rdiv; rewrite Rmult_1_l. rewrite <-(Rmult_1_r (/ 256)) at 1. apply Rmult_le_compat_l; [|apply pow_R1_Rle]; lra. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float