proposition: Theorem inbetween_float_round : forall rnd choice, ( forall x m l, inbetween_int m x l -> rnd x = choice m l ) -> forall x m l, let e := cexp beta fexp x in inbetween_float beta m e x l -> round beta fexp rnd x = F2R (Float beta (choice m l) e).
proof: Proof. intros rnd choice Hc x m l e Hl. unfold round, F2R. simpl. apply (f_equal (fun m => (IZR m * bpow e)%R)). apply Hc. apply inbetween_mult_reg with (bpow e). apply bpow_gt_0. now rewrite scaled_mantissa_mult_bpow. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket