fact: Definition unsplit {m n} (jk : 'I_m + 'I_n) := match jk with inl j => lshift n j | inr k => rshift m k end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)