proposition: Lemma ttakeK m1 m2 (t1 : m1.-tuple A) (t2 : m2.-tuple A) : ttake [tuple of t1 ++ t2] = t1.
proof: Proof. apply/val_eqP => /=. by rewrite ttakeE take_cat size_tuple ltnn subnn /= take0 cats0. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)