proposition: Lemma PI_RGT_0 : PI > 0.
proof: Proof. unfold PI; destruct pi2_int; lra. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg