proposition: Lemma injm_restrm : 'injm f -> 'injm fA.
proof: Proof. by apply: subset_trans; rewrite ker_restrm subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)