proposition: Lemma PI_tg_pos : forall n:nat, 0 <= PI_tg n.
proof: Proof. intro; unfold PI_tg; left; apply Rinv_0_lt_compat; apply lt_INR_0; replace (2 * n + 1)%nat with (S (2 * n)); [ apply Nat.lt_0_succ | ring ]. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra