proposition: Theorem Zorn_lemma r: order r -> inductive r -> exists a, maximal r a.
proof: Proof. move=> or isr; apply: Zorn_aux =>//. by move=> s ssr wo; hnf; apply: isr =>//; apply: worder_total. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)