proposition: Lemma ordering_function_least_least : forall B f , ordering_function f ordinal B -> least_member lt B (f zero).
proof: Proof. Proof with auto with schutte. intros b f H; case H; intros H0 H2 H3 H4 . split. - apply H2 ... - intros x H55. case (H3 _ H55); intros x0 (Hx0,H'x0); subst x. generalize (ordering_function_mono_weak H (a:=zero) (b:=x0)). intro H6; apply H6 ... Qed.
imports: ZornsLemma(CountableTypes)