fact: Definition enforce_helper (fexp : Z -> Z) (xi zi : FF) := Fle2 (lower zi) (round roundUP fexp (lower xi)) && Fle2 (round roundDN fexp (upper xi)) (upper zi).
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round