proposition: Lemma finite_set_prop1 a y: inc a y -> ((cardinal (y -s1 a)) <> (cardinal y) <-> finite_set y).
proof: Proof. move => ay. rewrite/finite_set - (setC1_K ay) csucc_pr1 (setC1_K ay). have cz := (CS_cardinal (y -s1 a)). split; last by move/(finite_succP cz) /finite_cP/proj2. by move=>h; apply/(finite_succP cz); apply/finite_cP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)