proposition: Theorem Q_positive: (0 < q)%R.
proof: Proof. case (Rle_or_lt q 0%R); auto; intros. absurd (3*(Rabs (p-q)) < (Rabs (p-q)))%R. apply Rle_not_lt; apply Rle_trans with (1*(Rabs (p-q)))%R; auto with real. apply Rmult_le_compat_r; auto with real. apply Rabs_pos. apply Rlt_le_trans with (1:=Secondcase). apply Rle_trans with (2:=Rabs_triang_inv p q). right; rewrite Rabs_right. rewrite Rabs_left1; auto with real; ring. apply Rle_ge; apply P_positive with bo precision b b'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz