proposition: Lemma PI2_3_2 : 3/2 < PI/2.
proof: Proof. apply PI2_lower_bound;[split; lra | ]. destruct (pre_cos_bound (3/2) 1) as [t _]; [lra | lra | ]. apply Rlt_le_trans with (2 := t); clear t. unfold cos_approx; simpl; unfold cos_term. rewrite !INR_IZR_INZ. cbv -[IZR]. field_simplify. apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia