proposition: Lemma cast_set_inj n m (H : n = m) : injective (cast_set H).
proof: Proof. by move=> S1 S2; rewrite /cast_set /=; apply: imset_inj; apply: cast_ord_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple) mathcomp(finset tuple bigop) tools