proposition: Theorem Fulp_le_twice_r_round: forall (x y:float) (r:R), (0 <= x)%R -> (Fbounded bo x) -> (Fnormal radix bo y) -> (- dExp bo <= Fexp y - 1)%Z -> (x<=2*r)%R -> (EvenClosest bo radix precision r y) -> ((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
proof: Proof. intros x y r H H0 H1 U H2 H3. assert (2*y=(Float (Fnum y) (Z.succ (Fexp y))))%R. unfold FtoRradix, FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Z.succ (Fexp y)))). 2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto. 2:unfold FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. 2:rewrite powerRZ_1; unfold radix; ring. 2:left; auto. 2:elim H1; intros H6 H5; elim H6; intros. 2:split; simpl; auto with zarith. 2:split; simpl; auto with zarith. apply LeFulpPos; auto with real. elim H1; intros H6 H5; elim H6; intros;split; simpl; auto with zarith. apply EvenClosestMonotone2 with x (2*r)%R; auto. unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto. apply EvenClosestRoundedModeP; auto. apply Twice_EvenClosest_Round; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz