proposition: Lemma infinite_setU1 X x: infinite_set X -> infinite_set (X +s1 x).
proof: Proof. move/infinite_setP => h; apply/infinite_setP. by apply: (cle_inf_inf h); apply: sub_smaller; move => t tx; apply: setU1_r. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)