proposition: Lemma morphim_trivm (G H : {group aT}) : trivm G @* H = 1.
proof: Proof. apply/setP=> /= y; rewrite inE; apply/idP/eqP=> [|->]; first by case/morphimP. by apply/morphimP; exists (1 : aT); rewrite /= ?group1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)