proposition: Lemma split_ordP m n (i : 'I_(m + n)) : split_ord_spec i (split i) (i < m).
proof: Proof. by case: splitP; [left|right]; apply: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)