proposition: Lemma helper n `{xs:∞A} : Str_nth (1 + n) xs ≡ hd (tl (Str_nth_tl n xs)).
proof: Proof. Admitted. Lemma gs_nth_rn n : Str_nth n s ≤ r^n * x₀. Proof. induction n using peano_naturals.nat_induction. rewrite nat_pow_0, rings.mult_1_l; compute; reflexivity. rewrite nat_pow_S. apply (ForAll_Str_nth_tl n) in gs. destruct gs as [[GS1 GS2] FA]. replace (hd (Str_nth_tl n s)) with (Str_nth n s) in GS2 by auto. replace (hd (tl (Str_nth_tl n s))) with (Str_nth (1+n) s) in GS2. transitivity (r * Str_nth n s); [assumption|]. rewrite <- associativity. apply (maps.order_preserving_nonneg (.*.) r). apply orders.lt_le. destruct Hr as [Ha Hb]. auto. assumption. apply helper. Admitted. End properties. Lemma gs_dnn `(gs: ARGeometricSeries s) : DecreasingNonNegative s. Proof. revert s gs. cofix FIX; intros s gs. constructor. now split; auto using gs_positive, gs_tl, gs_decreasing. now apply FIX, gs_tl. Qed.
imports: Limit abstract_algebra orders additional_operations streams series nat_pow