proposition: Lemma nth_etake (T : Type) a (s : seq T) n : nth a (etake s) n = nth a s n.*2.
proof: Proof. have [m leMm] := ubnP (size s); elim: m s leMm n => [[]//|m IH [|b [|c s]]] HS n. - by rewrite /= !nth_nil. - by case: n => [|n]; rewrite //= nth_nil. rewrite etake_cons otake_cons; case: n => //= n. rewrite ltnS in HS. by apply: IH; apply: leq_trans HS => /=. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)