proposition: Lemma Rgt_3PI2_0 : 0 < 3 * (PI / 2).
proof: Proof. apply Rmult_lt_0_compat; [ prove_sup0 | unfold Rdiv; apply Rmult_lt_0_compat; [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ] ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt