proposition: Lemma unsplitK {m n} : cancel (@unsplit m n) split.
proof: Proof. by move=> [j|k]; case: split_ordP => ? /eqP; rewrite eq_shift// => /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)