proposition: Lemma eLe: (Rabs e <= (powerRZ radix (t+Fexp x+Fexp y)) /2)%R.
proof: Proof. apply Rmult_le_reg_l with 2%R; auto with real zarith. replace (FtoRradix e) with (x*y-r)%R;[idtac|rewrite eeq; ring]. apply Rle_trans with (Fulp b radix t r). unfold FtoRradix; apply ClosestUlp; auto with zarith. apply Rle_trans with (powerRZ radix (t + Fexp x + Fexp y)); [idtac|simpl; right; field; auto with real]. unfold Fulp; apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Z.le_trans with (Fexp (Float (pPred (vNum b)) (t+Fexp x+Fexp y))); [idtac|simpl; auto with zarith]. apply Fcanonic_Rle_Zle with radix b t; auto with zarith. apply FnormalizeCanonic; auto with zarith. elim rDef; auto. replace (Float (pPred (vNum b)) (t + Fexp x + Fexp y)) with (FPred b radix t (Float (nNormMin radix t) (t+1+Fexp x+Fexp y))). apply FPredCanonic; auto with zarith. apply FcanonicNnormMin; auto with zarith. rewrite FPredSimpl2; auto with zarith. simpl; unfold Z.pred; auto with zarith. replace (t+1+Fexp x +Fexp y+-1)%Z with (t+Fexp x+Fexp y)%Z; auto with zarith. simpl; auto with zarith. rewrite FnormalizeCorrect; auto with zarith. rewrite (Rabs_right (FtoR radix (Float (pPred (vNum b)) (t + Fexp x + Fexp y)))%R). 2: apply Rle_ge; apply LeFnumZERO; simpl; auto with zarith. 2: apply Zlt_le_weak; apply pPredMoreThanOne with radix t; auto with zarith. apply RoundAbsMonotoner with b t (Closest b radix) (x*y)%R; auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (Float (pPred (vNum b)) (t + Fexp x + Fexp y)) with (FPred b radix t (Float (nNormMin radix t) (t+1+Fexp x+Fexp y))). apply FBoundedPred; auto with zarith. elim FnormalNnormMin with radix b t (t + 1 + Fexp x + Fexp y)%Z; auto with zarith. rewrite FPredSimpl2; auto with zarith. simpl; unfold Z.pred; auto with zarith. replace (t+1+Fexp x +Fexp y+-1)%Z with (t+Fexp x+Fexp y)%Z; auto with zarith. simpl; auto with zarith. rewrite Rabs_mult. apply Rle_trans with ((FtoRradix (Float (pPred (vNum b)) (Fexp x)))*(powerRZ radix (t+Fexp y)))%R. apply Rmult_le_compat; try apply Rabs_pos; auto with real zarith. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith. unfold FtoR, Fabs; simpl. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. elim Nx; intros I1 I2; elim I1; intros; unfold pPred; auto with real zarith. apply IZR_le; lia. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith. unfold FtoR, Fabs; simpl. rewrite powerRZ_add. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. elim Ny; intros I1 I2; elim I1; intros; apply Rle_trans with (IZR (Zpos (vNum b))); auto with real zarith. apply IZR_le; lia. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. apply IZR_neq; lia. unfold FtoRradix, FtoR; simpl; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; right; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz