proposition: Lemma injm_morphim_inj A B : A \subset D -> B \subset D -> f @* A = f @* B -> A = B.
proof: Proof. by move=> sAD sBD eqAB; rewrite -(injmK sAD) eqAB injmK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)