proposition: Lemma Str_nth_everyOther (n : nat) (s : ∞A) : Str_nth n (everyOther s) = Str_nth (2 * n) s.
proof: Proof. unfold Str_nth. rewrite Str_nth_tl_everyOther. reflexivity. 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