proposition: Lemma ClosestZero2: forall (r:R) (x:float), (Closest bo radix r x) -> (r=0)%R -> (FtoRradix x=0)%R.
proof: Proof. intros. cut (0 <= FtoRradix x)%R;[intros |idtac]. cut (FtoRradix x <= 0)%R;[intros; auto with real |idtac]. unfold FtoRradix; apply RleRoundedLessR0 with bo p (Closest bo radix) r; auto with real. apply ClosestRoundedModeP with p; auto with zarith. unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) r; auto with real. apply ClosestRoundedModeP with p; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz