proposition: Lemma nth_otake (T : Type) a (s : seq T) n : nth a (otake s) n = nth a s n.*2.+1.
proof: Proof. by case: s; rewrite //= ?nth_nil // => _ s; rewrite nth_etake. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)