proposition: Lemma max_card_on_set_unique X k1 k2: max_card_on_set X k1 -> max_card_on_set X k2 -> k1 = k2.
proof: Proof. move => [[x1 x1X x1v] h1] [[x2 x2X x2v] h2]. by move: (h1 x2 x2X) (h2 x1 x1X); rewrite x1v x2v => l1 l2; apply: cleA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)