proposition: Lemma cat_ttake_tdrop m (t : (m + m).-tuple A) : t = [tuple of ttake t ++ tdrop t].
proof: Proof. by apply/val_eqP; rewrite /= ttakeE tdropE; rewrite cat_take_drop. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)