proposition: Lemma LeExpRound2: forall (n:Z) (f g:float), Closest bo radix f g -> (n <= Fexp f)%Z -> exists g':float, Fbounded bo g' /\ FtoRradix g'=g /\ (n <= Fexp g')%Z.
proof: Proof. intros. elim LeExpRound with f g; auto. intros g' T; elim T; intros T1 T2; elim T2; intros T3 T4; clear T T2. exists g'; split; auto; split; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz