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