proposition: Theorem Zorn_aux r: order r -> (forall s, sub s (substrate r) -> worder (induced_order r s) -> (bounded_above r s)) -> exists a, maximal r a.
proof: Proof. move=> or zaux. set E := substrate r. ex_middle bad. have Ha: forall x, inc x E -> exists y, glt r x y. move => x xR; ex_middle ba1; case: bad; exists x; split => //. by move => y le1; symmetry; ex_middle ba2; case: ba1; exists y. pose next x := choose (fun y => glt r x y). have ha: (forall x, inc x (substrate r) -> glt r x (next x)). move=> x xE; apply: (choose_pr (Ha _ xE)). pose p s x := upper_bound r s x. pose max s := choose (p s). have hb: (forall s, sub s (substrate r) -> worder (induced_order r s) -> upper_bound r s (max s)). by move => s sa sb;move:(zaux _ sa sb) => xx; apply: choose_pr. case: (Zorn_aux_eff or hb ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)