fact: Definition mul_helper (xi yi zi : FF) := let xly := FImult2 (lower xi) yi in let xuy := FImult2 (upper xi) yi in Fle2 (lower zi) (lower xly) && Fle2 (lower zi) (lower xuy) && Fle2 (upper xly) (upper zi) && Fle2 (upper xuy) (upper zi).
imports: Gappa_common Gappa_pred_bnd