CoRN.reals.fast.CRpi

Require Export CRpi_fast.
Require Import CRsign.

Lemma CRpi_pos : (0 < CRpi)%CR.
Proof. CR_solve_pos (1#10)%Qpos. Qed.