proposition: Lemma Str_nth_tl_everyOther (n : nat) (s : ∞A) : Str_nth_tl n (everyOther s) ≡ everyOther (Str_nth_tl (2 * n) s).
proof: Proof. revert s. induction n; intros s; simpl; trivial. rewrite IHn. replace (n + S (n + 0))%nat with (S (2*n))%nat. easy. change (1 + (1 + 1) * n = n + (1 + (n + 0))). ring. 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