proposition: Lemma infinite_set_pr2 x: infinite_o x -> ~(inc x x) -> infinite_set x.
proof: Proof. rewrite /infinite_o/osucc => /EqS eq1 /setU1_K eq2. rewrite - eq2; apply: infinite_set_pr1 ; [ fprops | ue ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)