proposition: Lemma trivial_isog : G :=: 1 -> H :=: 1 -> G \isog H.
proof: Proof. move=> -> ->; apply/isogP. exists [morphism of @trivm gT hT 1]; rewrite /= ?morphim1 //. by rewrite ker_trivm; apply: subxx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)