proposition: Lemma max_card_on_set_exists X n: natp n -> nonempty X -> (forall x, inc x X -> cardinal x <=c n) -> exists2 k, natp k & max_card_on_set X k.
proof: Proof. move=> nN neX hyp. set T := fun_image X cardinal. have pa: (forall m, inc m T -> m <=c n) by move => m/funI_P [z /hyp zX ->]. have neT: nonempty T by apply: funI_setne. have TN: sub T Nat by move => m /pa /NS_le_nat; apply. have fT: finite_set T. by apply: sub_finite_set (finite_Nintcc \0c n) => t /pa /(NintcP nN). move: (finite_subset_Nat TN fT neT) => [m mT mg]. have mN: natp m by apply: TN. move /funI_P:mT => [x mb mp]. have he: exists2 x, inc x X & cardinal x = m by ex_tac. exists m => //;split => // t ts; apply: mg; apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)