proposition: Lemma otakeK (T : Type) (s1 s2 : seq T) : size s1 = size s2 -> otake (eocat s1 s2) = s2.
proof: Proof. elim: s1 s2 => [[]//|a s1 IH [|b s2] //]. by rewrite [eocat _ _]/= otake_cons etake_cons /= => [] [/IH->]. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)