proposition: Lemma morphim_inj G H : ('ker f \subset G) && (G \subset D) -> ('ker f \subset H) && (H \subset D) -> f @* G = f @* H -> G :=: H.
proof: Proof. by move=> nsGf nsHf /morphim_injG->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)