proposition: Theorem rndG_conversion : forall rdir rexp f, float2R (round (rndG_g rdir) rexp f) = Generic_fmt.round radix2 rexp (rndG_f rdir) (float2R f).
proof: Proof. intros (rf, rg, req) rexp f. simpl. rewrite rndG_conversion_aux. now apply round_ext. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux