proposition: Lemma leq_homg rT aT (C : {set rT}) (G : {group aT}) : homg C G -> #|C| <= #|G|.
proof: Proof. by case/homgP=> f <-; apply: leq_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)