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