proposition: Theorem Q_le_two_P: (q <= 2*p)%R.
proof: Proof. fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl. apply Rle_trans with (3*q-q)%R; [right; ring|idtac]. pattern (FtoRradix q) at 1; rewrite <- (Rabs_right q). 2: apply Rle_ge; generalize Q_positive; auto with real. pattern (FtoRradix q) at 1; replace (FtoRradix q) with (-(p-q)+p)%R;[idtac|ring]. apply Rle_trans with (3*(Rabs (-(p-q))+(Rabs p))-q)%R. unfold Rminus; apply Rplus_le_compat_r. apply Rmult_le_compat_l; auto with real. apply Rabs_triang. rewrite Rabs_Ropp. rewrite (Rabs_right p). 2:apply Rle_ge; apply P_positive with bo precision b b'; auto. apply Rle_trans with (3 * (Rabs (p - q)) + (3*p - q))%R;[right;ring|idtac]. apply Rle_trans with (p+q+(3*p-q))%R; auto with real. right;ring. Qed.
imports: Reals ZArith List PeanoNat Psatz