proposition: Theorem round_any_correct : forall x m e l, inbetween_float beta m e x l -> (e = cexp beta fexp x \/ (l = loc_Exact /\ format x)) -> round beta fexp rnd x = F2R (Float beta (choice m l) e).
proof: Proof. Proof with auto with typeclass_instances. intros x m e l Hin [He|(Hl,Hf)]. rewrite He in Hin |- *. apply inbetween_float_round with (2 := Hin). exact inbetween_int_valid. rewrite Hl in Hin. inversion_clear Hin. rewrite Hl. replace (choice m loc_Exact) with m. rewrite <- H. apply round_generic... rewrite <- (Zrnd_IZR rnd m) at 1. apply inbetween_int_valid. now constructor. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket