proposition: Theorem inbetween_float_round_sign : forall rnd choice, ( forall x m l, inbetween_int m (Rabs x) l -> rnd x = cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l) ) -> forall x m l, let e := cexp beta fexp x in inbetween_float beta m e (Rabs x) l -> round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
proof: Proof. intros rnd choice Hc x m l e Hx. apply (f_equal (fun m => (IZR m * bpow e)%R)). simpl. replace (Rlt_bool x 0) with (Rlt_bool (scaled_mantissa beta fexp x) 0). apply Hc. apply inbetween_mult_reg with (bpow e). apply bpow_gt_0. rewrite <- (Rabs_right (bpow e)) at 3. rewrite <- Rabs_mult. now rewrite scaled_mantissa_mult_bpow. apply Rle_ge. apply bpow_ge_0. destruct (Rlt_bool_spec x 0) as [Zx|Zx] ; simpl. apply Rlt_bool_true. rewrite <- (Rmult_0_l (bpow (-e))). apply Rmult_lt_compat_r with (2 := Zx). apply bpow_gt_0. apply Rlt_bool_false. apply Rmult_le_pos with (1 := Zx). apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket