proposition: Lemma the_max_card_on_set_prop X n (k := the_max_card_on_set X): natp n -> nonempty X -> (forall x, inc x X -> cardinal x <=c n) -> max_card_on_set X k /\ natp k.
proof: Proof. move => ha hb hc; apply: select_pr. apply: (max_card_on_set_exists ha hb hc). move => i j _ iv _ jv; apply:(max_card_on_set_unique iv jv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)