proposition: Theorem Fulp_le_twice_r: forall x y:float, (0 <= x)%R -> (Fnormal radix bo y) -> (Fbounded bo x) -> (x<=2*y)%R -> ((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
proof: Proof. intros. 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 H0; intros H6 H5; elim H6; intros. 2:split; auto with zarith. 2:split; simpl; auto with zarith. apply LeFulpPos; auto with real. elim H0; intros H6 H5; elim H6; intros;split; simpl; auto with zarith. fold FtoRradix; rewrite <- H3; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz