proposition: Lemma Ratan_seq_decreasing : forall x, (0 <= x <= 1)%R -> Un_decreasing (Ratan_seq x).
proof: Proof. intros x Hx n. unfold Ratan_seq, Rdiv. apply Rmult_le_compat. - apply pow_le. exact (proj1 Hx). - apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. lia. - destruct (proj1 Hx) as [Hx1|Hx1]. 1:destruct (proj2 Hx) as [Hx2|Hx2]. + rewrite <- (Rinv_inv x). repeat rewrite (pow_inv (/ x)). apply Rlt_le. apply Rinv_lt_contravar. { apply Rmult_lt_0_compat ; apply pow_lt ; auto with real. } apply Rlt_pow. { rewrite <- Rinv_1. apply Rinv_lt_contravar. { rewrite Rmult_1_r. exact Hx1. } exact Hx2. } lia. + rewrite Hx2. do 2 rewrite pow1. apply Rle_refl. + rewrite <- Hx1. do 2 (rewrite pow_i ; [ idtac | lia ]). apply Rle_refl. - apply Rlt_le. apply Rinv_lt_contravar. { apply Rmult_lt_0_compat ; apply lt_INR_0 ; lia. } apply lt_INR. lia. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia