fact: Definition div_pp_helper (xi yi zi : FF) := Fpos (lower yi) && Fpos0 (lower xi) && Fle2 (Fmult2 (upper yi) (lower zi)) (lower xi) && Fle2 (upper xi) (Fmult2 (lower yi) (upper zi)).
imports: Gappa_common Gappa_decimal