proposition: Lemma the_max_card_on_set_prop2 X n: natp n -> max_card_on_set X n -> the_max_card_on_set X = n.
proof: Proof. move => ha hb. have H: singl_val2 (inc^~ Nat) (max_card_on_set X). by move => a b /= _ ax _ bx; apply: (max_card_on_set_unique ax bx). have exx:(exists2 x, inc x Nat & max_card_on_set X x) by exists n. move: (select_pr exx H); rewrite /the_max_card_on_set; set y := select _ _. by move => [h1 _]; move: (max_card_on_set_unique h1 hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)