proposition: Lemma split3app n3 n2 n1 p1 p2 p3 : split3 n1 n2 n3 (p1 ## p2 ## p3) = (p1,p2,p3).
proof: Proof. by rewrite /split3 !split2app. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec