proposition: Lemma z_infinite_nat3 X: z_infinite X -> sub Nat X.
proof: Proof. move=> [h1 h2]; apply: Nat_induction => // n nN nx. by rewrite (succ_of_nat nN); apply: h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)