proposition: Lemma homg_refl aT (A : {set aT}) : homg A A.
proof: Proof. by apply/homgP; exists (idm_morphism A); rewrite im_idm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)