proposition: Lemma yLe2x: ~(FtoRradix x=0)%R -> (Rabs y <= 2*Rabs x)%R.
proof: Proof. case (Rle_or_lt (Rabs b) (Rabs a)); intros. unfold FtoRradix; apply yLe2x_aux with bo p a b e; auto. unfold FtoRradix; apply yLe2x_aux with bo p b a e; auto with real; fold FtoRradix. rewrite Rplus_comm; auto. replace (b+a+e)%R with (a+b+e)%R; auto; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz