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
.