proposition: Lemma eocat_etake_otake (T : Type) n (s : seq T) : size s = n + n -> eocat (etake s) (otake s) = s.
proof: Proof. elim: n s =>[[]// | n IH [//|a [|b s]]]; rewrite !addnS //. by rewrite !(etake_cons, otake_cons) /= => [] [H]; rewrite IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)