proposition: Lemma eotcatK (T : Type) (s : seq T) : eotcat (etake s) (otake s) = s.
proof: Proof. have [n leMs] := ubnP (size s). elim: n s leMs => //= n IH [|a[|b s]] //= sLn. by rewrite IH // -ltnS ltnW. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)