proposition: Lemma empty_ordering : forall B, (forall b, ~ B b) -> ordering_function (fun o => o) (members zero) B.
proof: Proof. intros B H; split. - intros a b H0 H1; destruct (not_lt_zero H0);auto. - intros b H0 ; now destruct (not_lt_zero H0). - intros x Hx; now destruct (H x). - intros a b Hb; case (@not_lt_zero a); assumption. Qed.
imports: ZornsLemma(CountableTypes)