proposition: Lemma sin_PI2 : sin (PI / 2) = 1.
proof: Proof. replace (PI / 2) with PI2 by (unfold PI; field). assert (int' : 0 < PI2 < 2). { destruct pi2_int; split; lra. } assert (lo2 := sin_pos_tech PI2 int'). assert (t2 : Rabs (sin PI2) = 1). { rewrite <- Rabs_R1; apply Rsqr_eq_abs_0. rewrite Rsqr_1, sin2, cos_pi2, Rsqr_0, Rminus_0_r; reflexivity. } revert t2; rewrite Rabs_pos_eq;[| apply Rlt_le]; tauto. 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