proposition: Lemma LeExpRound: forall f g:float, Closest bo radix f g -> exists g':float, Fbounded bo g' /\ FtoRradix g'=g /\ (Fexp f <= Fexp g')%Z.
proof: Proof. intros. case (Zle_or_lt (Fexp f) (Fexp g)); intros. exists g; split; auto. elim H; auto. elim RoundedModeRep with bo radix p (Closest bo radix) f g; auto with zarith. 2: apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; intros n H1. exists (Float n (Fexp f)). elim H; intros H2 T; clear T. split; split; simpl; auto with zarith real . apply Z.le_lt_trans with (Z.abs (Fnum g)); auto with zarith; try apply H2. apply le_IZR. apply Rmult_le_reg_l with (powerRZ radix (Fexp g)); auto with real zarith. apply powerRZ_lt, IZR_lt; auto with real zarith. apply Rle_trans with (Rabs g);[idtac| unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl; right; ring]. rewrite H1; unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl. rewrite Rmult_comm; apply Rmult_le_compat_l; auto with real zarith. apply IZR_le; auto with zarith. apply Rle_powerRZ; try apply IZR_le; auto with zarith. apply Z.le_trans with (Fexp g); auto with zarith; apply H2. Qed.
imports: Reals ZArith List PeanoNat Psatz