proposition: Lemma setP_minimal A F: sub A (\Po F) -> nonempty A -> (forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) -> sub S A -> nonempty S -> inc (intersection S) A) -> exists a, minimal (sub_order A) a.
proof: Proof. move=> Ap [x xA] pA. move: (sub_osr A) => [oA sr1]. move: (opp_osr oA) => [ooA soA]. have ioA: inductive (opp_order (sub_order A)). move => X; rewrite soA sr1 => XA;rewrite /total_order. rewrite iorder_sr // ? soA ? sr1 //. move=> [pb pc]; rewrite /upper_bound soA sr1. case: (emptyset_dichot X) => neX. exists x; rewrite neX;split => // y; case; case. have iXA:inc (intersection X) A. apply: pA =>// a b aX bX. by move: (pc _ _ aX bX); case => h; move: (iorder_gle1 h) => /igraph_pP /sub_gleP [_ _]; [right | left]. exists (intersection X); saw. move=> y yX;apply /igraph_pP; apply /sub_gleP;split; fprops. by apply: setI_s1. move: (Zorn_lemma ooA ioA)=> [a ] /(maximal_opp oA) ha. by exists a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)