proposition: Lemma rExp: (t - 1 + Fexp x + Fexp y <= Fexp r)%Z.
proof: Proof. apply Z.le_trans with (Fexp (Float (nNormMin radix t) (t-1+Fexp x+Fexp y))); [simpl; auto with zarith|idtac]. apply Z.le_trans with (Fexp (Fnormalize radix b t r)). apply Fcanonic_Rle_Zle with radix b t; auto with zarith. apply FcanonicNnormMin; auto with zarith. apply FnormalizeCanonic; auto with zarith. elim rDef; auto. rewrite FnormalizeCorrect; auto with zarith. rewrite (Rabs_right (FtoR radix (Float (nNormMin radix t) (t-1 + Fexp x + Fexp y)))%R). 2: apply Rle_ge; apply LeFnumZERO; simpl; auto with zarith. 2: unfold nNormMin; auto with zarith. apply RoundAbsMonotonel with b t (Closest b radix) (x*y)%R; auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. apply FcanonicBound with radix; auto with zarith. apply FcanonicNnormMin; auto with zarith. fold FtoRradix; replace (FtoRradix (Float (nNormMin radix t) (t-1 + Fexp x + Fexp y))) with ((Float (nNormMin radix t) (Fexp x))*(Float (nNormMin radix t) (Fexp y)))%R. rewrite Rabs_mult. apply Rmult_le_compat. unfold FtoRradix; apply LeFnumZERO; simpl; unfold nNormMin; try apply Zpower_NR0; auto with zarith. unfold FtoRradix; apply LeFnumZERO; simpl; unfold nNormMin; try apply Zpower_NR0; auto with zarith. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith; unfold FtoR; simpl. apply Rmult_le_compat_r; auto with real zarith; apply Rmult_le_reg_l with (IZR radix); try apply IZR_lt; auto with real zarith. apply Rmult_le_compat_l. apply IZR_le; lia. apply powerRZ_le, IZR_lt; lia. rewrite <- mult_IZR; rewrite <- (PosNormMin radix b t); auto with zarith. elim Nx; intros I1 I2; rewrite Zabs_Zmult in I2; rewrite Z.abs_eq in I2; auto with real zarith. rewrite <- mult_IZR; apply IZR_le; auto with real zarith. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith; unfold FtoR; simpl. apply Rmult_le_compat_r; auto with real zarith; apply Rmult_le_reg_l with (IZR radix); try apply IZR_lt; auto with real zarith. apply Rmult_le_compat_l. apply IZR_le; lia. apply powerRZ_le, IZR_lt; lia. rewrite <- mult_IZR; rewrite <- (PosNormMin radix b t); auto with zarith. elim Ny; intros I1 I2; rewrite Zabs_Zmult in I2; rewrite Z.abs_eq in I2; auto with real zarith. rewrite <- mult_IZR; apply IZR_le; auto with real zarith. unfold FtoRradix, FtoR; simpl. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. replace (IZR (nNormMin radix t)) with (powerRZ radix (t-1));[ring|idtac]. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ. rewrite inj_pred; auto with zarith; unfold Z.pred; auto with real zarith. apply Zpower_NR0; lia. apply FcanonicLeastExp with radix b t; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. elim rDef; auto. apply FnormalizeCanonic; auto with zarith; elim rDef; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz