proposition: Lemma card_setC1_inf E x: infinite_set E -> cardinal E = cardinal (E -s1 x).
proof: Proof. move => iE; symmetry;apply:infinite_compl => //. rewrite cardinal_set1; apply: (clt_fin_inf finite_1). by apply/infinite_setP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)