proposition: Theorem card_eqP x y: x =c y <-> x \Eq y.
proof: Proof. move: (cardinal_pr1 x) (cardinal_pr1 y) => [ox exp lx][oy eyp ly]. split => h; first by apply: (EqT exp); rewrite h; exact:(EqS eyp). apply: extensionality. exact: (lx _ oy (EqT h eyp)). exact: (ly _ ox (EqT (EqS h) exp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)