fact: Definition tsplit {m n} (i : 'I_(m + n)) : 'I_m + 'I_n := match ltnP (i) n with | LtnNotGeq lt_i_n => inr _ (Ordinal lt_i_n) | GeqNotLtn ge_i_n => inl _ (Ordinal (tsplit_subproof ge_i_n)) end.
imports: mathcomp(all_ssreflect finmap)