proposition: Lemma CRpi_pos : (0 < CRpi)%CR.
proof: Proof. CR_solve_pos (1#10)%Qpos. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRpi_fast CoRN.reals.fast.CRsign