proposition: Lemma card_card x: cardinalp x -> cardinal x = x.
proof: Proof. move=> [cx1 cx2]. have aux:= (cardinal_pr1 x). have aux': cardinal_prop x x by split; fprops. apply: (cardinal_unique aux aux'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)