proposition: Lemma pow_lt_1_compat : forall x n, 0 <= x < 1 -> (0 < n)%nat -> 0 <= x ^ n < 1.
proof: Proof. intros x n hx; induction 1; simpl. { rewrite Rmult_1_r; tauto. } split. { apply Rmult_le_pos; tauto. } rewrite <- (Rmult_1_r 1); apply Rmult_le_0_lt_compat; intuition. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia