fact: Definition round_helper (rnd : float2 -> float2) (xi zi : FF) := Fle2 (lower zi) (rnd (lower xi)) && Fle2 (rnd (upper xi)) (upper zi).
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round