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