proposition: Lemma ltn_morphim A : [1] \proper 'ker_A f -> #|f @* A| < #|A|.
proof: Proof. case/properP; rewrite sub1set => /setIP[A1 _] [x /setIP[Ax kx] x1]. rewrite (cardsD1 1 A) A1 ltnS -{1}(setD1K A1) morphimU morphim1. rewrite (setUidPr _) ?sub1set; last first. by rewrite -(mker kx) mem_morphim ?(dom_ker kx) // inE x1. by rewrite (leq_trans (leq_imset_card _ _)) ?subset_leq_card ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)