proposition: Lemma inn_Str_nth (s : ∞A) : IncreasingNonNegative s ↔ ∀ n, 0 ≤ Str_nth n s ≤ Str_nth (S n) s.
proof: Proof. split. intros E n. revert s E. induction n; intros s E; unfold Str_nth in *; simpl. apply E. apply IHn. now destruct E. revert s. cofix FIX. intros s E. constructor; unfold Str_nth in *; simpl in *. apply (E O). apply FIX. intros n. apply (E (S n)). Qed.
imports: Coq.setoid_ring.Ring Coq.Arith.Factorial MathClasses.misc.workaround_tactics MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.nat_pow MathClasses.theory.int_pow MathClasses.theory.streams