proposition: Lemma cardinal_supremum1 x: cardinal_set x -> exists! b, [/\ cardinalp b, (forall a, inc a x -> a <=c b) & (forall c, cardinalp c -> (forall a, inc a x -> a <=c c) -> b <=c c)].
proof: Proof. move=> alc. move: (CS_sup alc) (card_sup_ub alc) => pa pb. apply /unique_existence; split. by exists (union x); split => // y cy; apply:(card_ub_sup). move=> u v [cu up1 up2][cv vp1 vp2]. exact: (cleA (up2 _ cv vp1) (vp2 _ cu up1)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)