proposition: Lemma infinite_set_pr a b: inc b a -> a \Eq (a -s1 b) -> infinite_set a.
proof: Proof. move=> /csucc_pr2 ba /card_eqP eq; apply/card_eqP. by rewrite {1} ba - eq card_csucc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)