proposition: Theorem Half_Closest_Round: forall (x:float) (r:R), (- dExp bo <= Z.pred (Fexp x))%Z -> (Closest bo radix r x) -> (Closest bo radix (r/2)%R (Float (Fnum x) (Z.pred (Fexp x)))).
proof: Proof. intros x r L H. assert (x/2=(Float (Fnum x) (Z.pred (Fexp x))))%R. unfold FtoRradix, FtoR, Z.pred; simpl; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 3; simpl; unfold radix; field. elim H; intros H2 H3. split; [split; simpl; auto with zarith; apply H2|idtac]. intros. fold FtoRradix; rewrite <- H0. replace (x/2-r/2)%R with (/2*(x-r))%R;[idtac|unfold Rdiv; ring]. rewrite Rabs_mult; rewrite Rabs_right; auto with real. 2: apply Rle_ge; auto with real. replace (f-r/2)%R with (/2*((Float (Fnum f) (Z.succ (Fexp f)))-r))%R. rewrite Rabs_mult; rewrite Rabs_right with (/2)%R. 2: apply Rle_ge; auto with real. apply Rmult_le_compat_l; auto with real. unfold FtoRradix; apply H3. destruct H1; split; simpl; auto with zarith. unfold FtoRradix, FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; field. Qed.
imports: Reals ZArith List PeanoNat Psatz