proposition: Lemma underf_mult_aux': forall x y, Fbounded b x -> Fbounded b y -> (bpow beta (-dExp b + 2 * prec - 1)%Z <= Rabs (FtoR beta x * FtoR beta y)) -> (-dExp b <= Pff.Fexp x + Pff.Fexp y)%Z.
proof: Proof. intros. now apply underf_mult_aux. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat