proposition: Lemma cardinal_unique x y z: cardinal_prop x y -> cardinal_prop x z -> y = z.
proof: Proof. move=> [oy exy p1] [oz exz p2]. by apply: extensionality; [ apply: p1 | apply: p2 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)