proposition: Lemma codom_perm (g: {ffun 'I_k -> 'I_l}) (p: 'S_k) : forall x, (x \in codom (finfun (g \o p))) = (x \in codom g).
proof: Proof. move => x. apply/imageP/imageP. - case => /= y h1; rewrite ffunE => h2. by exists (p y). case => y h1 h2. exists (p^-1 y)%g => //=. by rewrite ffunE /= permKV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor