proposition: Lemma z_infinite_I X: z_infinite X -> z_omega X = Nat.
proof: Proof. move => ha. move: (z_omega_prop ha) => [qa qb]. apply: extensionality; last by apply: (z_infinite_nat3 qa). apply: (qb _ z_infinite_nat2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)