proposition: Lemma inv_g_of_fxE (g f: {ffun 'I_k -> 'I_l}) : same_codom f g -> forall x, g (inv_g_of_fx g f x) = f x.
proof: Proof. rewrite /inv_g_of_fx => heq. - case: same_codomP => h x. by rewrite !ffunE f_iinv. by case: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor