proposition: Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.
proof: Proof. assert (H := PI_RGT_0). 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