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