proposition: Lemma split2app n2 n1 p1 p2 : split2 n1 n2 (p1 ## p2) = (p1,p2).
proof: Proof. by rewrite /split2 high_catB low_catB. 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