proposition: Lemma perm_fE (g f: {ffun 'I_k -> 'I_l}) : injective f -> same_codom f g -> forall x, f x = g ((perm_f g f) x).
proof: Proof. move => hf hc /= x. rewrite /perm_f unlock /=. case: goodP => [/= _|[]] //. by rewrite inv_g_of_fxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor