proposition: Lemma etake_nseq (T : Type) i (a : T) : etake (nseq i a) = nseq (uphalf i) a.
proof: Proof. have [n leMi] := ubnP i; elim: n i leMi => // n IH [|[|i]] //= iLn. by rewrite IH // -ltnS (leq_trans _ iLn). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)