proposition: Lemma nth_eocat (T : Type) a (s1 s2 : seq T) n : size s1 = size s2 -> nth a (eocat s1 s2) n = nth a (if odd n then s2 else s1) n./2.
proof: Proof. elim: s1 s2 n => /= [[]//= n|b s1 IH [//= n|c s2 [|[|n]] //= [Hs]/=]]. by rewrite if_same !nth_nil. by rewrite negbK IH; case: odd. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)