proposition: Lemma inv_g_of_fx_inj (g f: {ffun 'I_k -> 'I_l}): injective f -> same_codom f g -> injectiveb (inv_g_of_fx g f).
proof: Proof. move => hf hc. apply/injectiveP => x y heq. apply: hf. by rewrite -!(inv_g_of_fxE hc) heq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor