proposition: Lemma eq_size_etake (T : Type) (s1 s2 : seq T) : size s1 = size s2 -> size (etake s1) = size (etake s2).
proof: Proof. have [k leMl] := ubnP (size s1). elim: k s1 s2 leMl => // k IH [|a [|b s1]] [|c [|d s2]] //= ss1Lk [] /IH -> //. by rewrite -ltnS ltnW. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)