proposition: Lemma etake_eocat (T : Type) (s1 s2 : seq T) : etake (eocat s1 s2) = s1.
proof: Proof. have [n leMs1] := ubnP (size s1). elim: n s1 leMs1 s2 => // n IH [|a[|b s1]] //= slLn s2. by rewrite IH // -ltnS (leq_trans _ slLn). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)