proposition: Lemma vLe: (Rabs v <= powerRZ radix (Fexp z)*radix)%R.
proof: Proof. assert (powerRZ radix (Fexp z) * radix=Float radix (Fexp z))%R. unfold FtoRradix, FtoR; simpl; ring. rewrite H. unfold FtoRradix; apply RoundAbsMonotoner with bo p (Closest bo radix) (pl+ul)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim zDef; intros I1 I2; elim I1; intros; split; simpl; auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Z.lt_trans with (pPred (vNum bo)); [apply pPredMoreThanRadix with p|unfold pPred]; auto with zarith. fold FtoRradix; rewrite <- H; apply vLe_aux. Qed.
imports: Reals ZArith List PeanoNat Psatz