proposition: Lemma ker_trivg_morphim A : (A \subset 'ker f) = (A \subset D) && (f @* A \subset [1]).
proof: Proof. case sAD: (A \subset D); first by rewrite sub_morphim_pre. by rewrite subsetI sAD. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)