proposition: Lemma propositionZ_zermelo: proposition_Z -> forall x, exists r, worder_on r x.
proof: Proof. move => h x; case: (p_or_not_p (Sfinite x)); last by case/h. move:Nat_order_wor => wor [[f fab] _]. exact:(wor_from_injection wor fab). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)