proposition: Lemma Rlt_3PI2_2PI : 3 * (PI / 2) < 2 * PI.
proof: Proof. generalize PI2_RGT_0; intro H1; generalize (Rplus_lt_compat_l (3 * (PI / 2)) 0 (PI / 2) H1); replace (3 * (PI / 2) + PI / 2) with (2 * PI). - rewrite Rplus_0_r; intro H2; assumption. - rewrite <-Rplus_diag; pattern PI at 1 2; rewrite <-Rplus_half_diag; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt