proposition: Lemma Alt_PI_RGT_0 : 0 < Alt_PI.
proof: Proof. assert (H := Alt_PI_ineq 0). apply Rmult_lt_reg_l with (/ 4). - apply Rinv_0_lt_compat; prove_sup0. - rewrite Rmult_0_r; rewrite Rmult_comm. elim H; clear H; intros H _. unfold Rdiv in H; apply Rlt_le_trans with (sum_f_R0 (tg_alt PI_tg) (S (2 * 0))). + simpl; unfold tg_alt; simpl; rewrite Rmult_1_l; rewrite Rmult_1_r; apply Rplus_lt_reg_l with (PI_tg 1). rewrite Rplus_0_r; replace (PI_tg 1 + (PI_tg 0 + -1 * PI_tg 1)) with (PI_tg 0); [ unfold PI_tg | ring ]. simpl; apply Rinv_lt_contravar. * rewrite Rmult_1_l; replace (2 + 1) with 3; [ prove_sup0 | ring ]. * rewrite Rplus_comm; pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; prove_sup0. + assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra