proposition: Lemma PI_tg_decreasing : Un_decreasing PI_tg.
proof: Proof. unfold PI_tg, Un_decreasing; intro. apply Rmult_le_reg_l with (INR (2 * n + 1)). - apply lt_INR_0. replace (2 * n + 1)%nat with (S (2 * n)); [ apply Nat.lt_0_succ | ring ]. - rewrite Rinv_r. + apply Rmult_le_reg_l with (INR (2 * S n + 1)). * apply lt_INR_0. replace (2 * S n + 1)%nat with (S (2 * S n)); [ apply Nat.lt_0_succ | ring ]. * rewrite (Rmult_comm (INR (2 * S n + 1))); rewrite Rmult_assoc; rewrite Rinv_l. -- do 2 rewrite Rmult_1_r; apply le_INR. replace (2 * S n + 1)%nat with (S (S (2 * n + 1))). ++ apply Nat.le_trans with (S (2 * n + 1)); apply Nat.le_succ_diag_r. ++ ring. -- apply not_O_INR; discriminate. + apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n)); [ discriminate | ring ]. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra