proposition: Lemma splitP m n (i : 'I_(m + n)) : split_spec i (split i) (i < m).
proof: Proof. set lt_i_m := i < m; rewrite /split. by case: _ _ _ _ {-}_ lt_i_m / ltnP; [left | right; rewrite subnKC]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)