proposition: Lemma sub_infinite_set x y: sub x y -> infinite_set x -> infinite_set y.
proof: Proof. move => /sub_smaller le1 /infinite_setP ix; apply/infinite_setP. by apply: (cle_inf_inf ix le1). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)