proposition: Theorem Fulp_le_twice_l: forall x y:float, (0 <= x)%R -> (Fnormal radix bo x) -> (Fbounded bo y) -> (2*x<=y)%R -> (2*(Fulp bo radix precision x) <= (Fulp bo radix precision y))%R.
proof: Proof. intros. assert (2*x=(Float (Fnum x) (Z.succ (Fexp x))))%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 x) (Z.succ (Fexp x)))). right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto. unfold FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. elim H0; intros H4 H5; elim H4; intros. left; split; auto. split; simpl; auto with zarith. apply LeFulpPos; auto with real. elim H0; intros H4 H5; elim H4; intros;split; simpl; auto with zarith. fold FtoRradix; rewrite <- H3; apply Rmult_le_pos; auto with real. fold FtoRradix; rewrite <- H3; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz