proposition: Lemma ttake_otakeE n (t : ((n + n) + (n + n)).-tuple A) : ttake (totake t) = totake (ttake t).
proof: Proof. apply/val_eqP; rewrite /= !(ttakeE, totakeE). have nnE : n + n = (size t)./2. by rewrite size_tuple /= [in RHS]addnn doubleK. rewrite [X in _ == _ (_ X _)]nnE. have nE : n = (size t)./2./2. by rewrite size_tuple /= !addnn !doubleK. rewrite [X in take X _]nE take_otakeE //. by rewrite size_tuple /= addnn odd_double. by rewrite -nnE addnn odd_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)