proposition: Lemma ClosestZero1: forall (r:R) (f g:float), (Closest bo radix r f) -> (FtoRradix f=0)%R -> (r=g)%R -> (-dExp bo <= Fexp g)%Z -> (r=0)%R.
proof: Proof. intros. case (Req_dec r 0); auto; intros. absurd (powerRZ radix (-(dExp bo)) <= Rabs f)%R; auto. apply Rlt_not_le; rewrite H0; rewrite Rabs_R0; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with real zarith. apply Rle_trans with (FtoRradix (Float 1 (-(dExp bo)))). right; unfold FtoRradix, FtoR; simpl; ring. unfold FtoRradix; apply RoundAbsMonotonel with bo p (Closest bo radix) r; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. split; simpl; auto with zarith. rewrite pGivesBound; apply Z.le_lt_trans with (Zpower_nat radix 0); auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. rewrite H1; unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold FtoR; simpl; apply Rmult_le_compat; auto with real zarith. apply powerRZ_le, IZR_lt; auto with real zarith. apply IZR_le. case (Zle_lt_or_eq 0 (Z.abs (Fnum g))); auto with zarith; intros. absurd (Rabs r=0)%R. apply Rabs_no_R0; auto. rewrite H1; unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl. rewrite <- H4; simpl; ring. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz