proposition: Lemma PI2_RGT_0 : 0 < PI / 2.
proof: Proof. unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup ]. 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