proposition: Lemma underf_mult_aux: forall e x y, Fbounded b x -> Fbounded b y -> (bpow beta (e + 2 * prec - 1)%Z <= Rabs (FtoR beta x * FtoR beta y)) -> (e <= Pff.Fexp x + Pff.Fexp y)%Z.
proof: Proof. intros e x y Fx Fy H. assert (HH: forall z, Fbounded b z -> Rabs (FtoR beta z) < bpow beta (Pff.Fexp z + prec)). clear -precisionGt1 pGivesBound; intros z Hz. unfold FtoR; rewrite <- bpow_powerRZ. rewrite Rabs_mult, Rmult_comm. rewrite Rabs_right. 2: apply Rle_ge, bpow_ge_0. rewrite bpow_plus; apply Rmult_lt_compat_l. apply bpow_gt_0. destruct Hz as (T1,T2). rewrite pGivesBound in T1. rewrite <- abs_IZR, <- IZR_Zpower;[idtac|lia]. apply IZR_lt. apply Z.lt_le_trans with (1:=T1). rewrite Zpower_Zpower_nat; lia. assert (e+2*prec-1 < (Pff.Fexp x+prec) +(Pff.Fexp y +prec))%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=H). rewrite Rabs_mult, bpow_plus. apply Rmult_lt_compat. apply Rabs_pos. apply Rabs_pos. now apply HH. now apply HH. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat