proposition: Lemma xLe2y : (Rabs x <= 2*Rabs y)%R.
proof: Proof. case (Rle_or_lt (Rabs b) (Rabs a)); intros. unfold FtoRradix; apply xLe2y_aux2 with bo p a b e; auto. unfold FtoRradix; apply xLe2y_aux2 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