proposition: Lemma tsplitP m n (i : 'I_(m + n)) : tsplit_spec i (tsplit i) (i < n).
proof: Proof. set lt_i_n := i < n; rewrite /tsplit. by case: {-}_ lt_i_n / ltnP; [left |right; rewrite subnK]. Qed.
imports: mathcomp(all_ssreflect finmap)