proposition: Lemma PI_neq0 : PI <> 0.
proof: Proof. red in |- *; intro; assert (H0 := PI_RGT_0); rewrite H in H0; elim (Rlt_irrefl _ H0). 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