proposition: Lemma goodP (g f: {ffun 'I_k -> 'I_l}) : reflect (injective f /\ same_codom f g) (good g f).
proof: Proof. apply: (iffP andP). - case => /injectiveP h1 /forallP h2. split => // x. by rewrite (eqP (h2 x)). case => h1 h2. split; first by apply/injectiveP. by apply/forallP => x; rewrite (h2 x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor