proposition: Lemma setP_maximal A F: sub A (\Po F) -> (forall So, (forall x y, inc x So -> inc y So -> sub x y \/ sub y x) -> sub So A -> inc (union So) A) -> exists a, maximal (sub_order A) a.
proof: Proof. move=> Ap /(setP_inductive Ap). by move: (sub_osr A) => [oA sr1];apply: Zorn_lemma. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)