proposition: Lemma vLe_aux: (Rabs (pl+ul) <= powerRZ radix (Fexp z)*radix)%R.
proof: Proof. apply Rle_trans with (powerRZ radix (Fexp z+1)); [idtac|rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; ring]. apply Rle_trans with (Rabs pl+Rabs ul)%R;[apply Rabs_triang|idtac]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (Fexp ph)+powerRZ radix (Fexp uh))%R; [idtac|apply LeExp]. apply Rle_trans with (2*Rabs pl+2*Rabs ul)%R;[simpl; right; ring|idtac]. apply Rplus_le_compat. apply Rle_trans with (Fulp bo radix p ph). rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto]. apply Rle_trans with (Fulp bo radix p uh). rewrite ulDef; unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto]. Qed.
imports: Reals ZArith List PeanoNat Psatz