proposition: Lemma cast1 (f: {ffun 'I_k -> 'I_l}) : injective f -> k = #|codom f|.
proof: Proof. move => hf. by rewrite (card_codom hf) cardT /= size_enum_ord. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor