proposition: Theorem Underf_Err3_bis: forall (x x' y y' z' z:float) (rx ry epsx epsy:R), (4 <= p) -> vNum b=vNum b' -> (dExp b <= dExp b')%Z -> (Underf_Err x x' rx epsx) -> (Underf_Err y y' ry epsy) -> (epsx+epsy <= 7)%R -> (Fbounded b' z') -> (FtoRradix z'=x'-y')%R -> (Fexp z' <= Fexp x')%Z -> (Fexp z' <= Fexp y')%Z -> (Closest b radix (x-y) z) -> (Underf_Err z z' (x-y) (epsx+epsy)%R).
proof: Proof. intros. apply Underf_Err3 with x' y' rx ry; auto. apply Rle_trans with (1:=H4). apply Rle_trans with (8-1)%R;[right; ring|unfold Rminus; apply Rplus_le_compat_r]. apply Rle_trans with (powerRZ radix 3)%R; auto with real zarith. apply Rle_trans with (powerRZ 2 3)%R; auto with real zarith. simpl; right; ring. simpl; auto with real zarith. assert (2 <= radix)%R;[apply IZR_le; auto with real zarith|idtac]. ring_simplify (2*1)%R; ring_simplify (radix*1)%R. apply Rmult_le_compat; auto with real zarith. apply Rlt_le; apply Rmult_lt_0_compat; auto with real. apply Rle_powerRZ; try apply IZR_le; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz