proposition: Lemma tunsplitK {m n} : cancel (@tunsplit m n) tsplit.
proof: Proof. move=> jk; have:= ltn_tunsplit jk; rewrite leqNgt. by do [case: tsplitP; case: jk => //= i j] => [|/addIn] => /ord_inj->. Qed.
imports: mathcomp(all_ssreflect finmap)