diff --git a/_CoqProject b/_CoqProject index a4387ea7b4..ec70b6755c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -11,6 +11,7 @@ classical/all_classical.v classical/boolp.v classical/contra.v +classical/wochoice.v classical/classical_sets.v classical/mathcomp_extra.v classical/functions.v diff --git a/classical/Make b/classical/Make index 4d4fe74c81..888b31ef14 100644 --- a/classical/Make +++ b/classical/Make @@ -9,6 +9,7 @@ boolp.v contra.v +wochoice.v classical_sets.v mathcomp_extra.v functions.v diff --git a/classical/contra.v b/classical/contra.v index afbc5bb92c..0af6c4bab6 100644 --- a/classical/contra.v +++ b/classical/contra.v @@ -779,6 +779,76 @@ Hint View for move/ move_viewP|2. Hint View for move/ Internals.equivT_LR|2 Internals.equivT_RL|2. Hint View for apply/ Internals.equivT_RL|2 Internals.equivT_LR|2. Export (canonicals) Internals. +Canonical TypeForall. +Canonical PropForall. +Canonical SetForall. +Canonical wrap1Prop. +Canonical wrap1Type. +Canonical proper_nProp. +Canonical trivial_nProp. +Canonical True_nProp. +Canonical False_nProp. +Canonical not_nProp. +Canonical and_nProp. +Canonical and3_nProp. +Canonical and4_nProp. +Canonical and5_nProp. +Canonical or_nProp. +Canonical or3_nProp. +Canonical or4_nProp. +Canonical unary_and_rhs. +Canonical binary_and_rhs. +Canonical imply_nProp. +Canonical exists_nProp. +Canonical exists2_nProp. +Canonical inhabited_nProp. +Canonical forall_nProp. +Canonical proper_nBody. +Canonical nonproper_nBody. +Canonical bounded_nBody. +Canonical unbounded_nBody. +Canonical is_true_nProp. +Canonical true_neg. +Canonical true_pos. +Canonical false_neg. +Canonical false_pos. +Canonical id_neg. +Canonical id_pos. +Canonical negb_neg. +Canonical negb_pos. +Canonical neg_ltn_LHS. +Canonical neg_leq_LHS. +Canonical leq_neg. +Canonical eq_nProp. +Canonical bool_neq. +Canonical true_neq. +Canonical false_neq. +Canonical eqType_neq. +Canonical eq_op_pos. +Canonical Prop_wType. +Canonical proper_wType. +Canonical forall_wType. +Canonical inhabited_wType. +Canonical void_wType. +Canonical unit_wType. +Canonical pair_wType. +Canonical sum_wType. +Canonical sumbool_wType. +Canonical sumor_wType. +Canonical sig1_wType. +Canonical sig2_wType. +Canonical sigT_wType. +Canonical sigT2_wType. +Canonical proper_wProp. +Canonical forall_wProp. +Canonical trivial_wProp. +Canonical inhabited_wProp. +Canonical nand_false_bool. +Canonical nand_true_bool. +Canonical and_wProp. +Canonical or_wProp. +Canonical exists_wProp. +Canonical exists2_wProp. (******************************************************************************) (* Lemma and tactic assume_not: add a goal negation assumption. The tactic *) diff --git a/classical/wochoice.v b/classical/wochoice.v new file mode 100644 index 0000000000..c75343a393 --- /dev/null +++ b/classical/wochoice.v @@ -0,0 +1,333 @@ +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import boolp contra. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Section LocalProperties. + +Context {T1 T2 T3 : Type} {T : predArgType}. +Implicit Type A : {pred T}. + +Local Notation "{ 'allA' P }" := (forall A : {pred T}, P A : Prop) (at level 0). +Local Notation ph := (phantom _). + +Definition prop_within d P & ph {allA P} := forall A, sub_mem (mem A) d -> P A. + +Lemma withinW A P : {allA P} -> prop_within (mem A) (inPhantom {allA P}). +Proof. by move=> allP ? _; apply: allP. Qed. + +Lemma withinT P : prop_within (mem T) (inPhantom {allA P}) -> {allA P}. +Proof. by move=> allP A; apply: allP. Qed. + +Lemma sub_within d d' P : + sub_mem d d' -> forall phP, @prop_within d' P phP -> @prop_within d P phP. +Proof. by move=> sdd' phP Pd' A /(_ _ _)/sdd'-/Pd'. Qed. + +End LocalProperties. + +Notation "{ 'in' <= S , P }" := + (prop_within (mem S) (inPhantom P)) : type_scope. + +Section RelDefs. + +Variables (T : Type) (R : rel T). +Implicit Types (x y z : T) (A C : {pred T}). + +(* TOTHINK: This should be ported to mathcomp. *) +Definition maximal z := forall x, R z x -> R x z. + +Definition minimal z := forall x, R x z -> R z x. + +Definition upper_bound A z := {in A, forall x, R x z}. + +Definition lower_bound A z := {in A, forall x, R z x}. + +Definition preorder := reflexive R /\ transitive R. + +Definition partial_order := preorder /\ antisymmetric R. + +Definition total_order := partial_order /\ total R. + +Definition nonempty A := exists x, x \in A. + +Definition minimum_of A z := z \in A /\ lower_bound A z. + +Definition maximum_of A z := z \in A /\ upper_bound A z. + +Definition well_order := forall A, nonempty A -> exists! z, minimum_of A z. + +Definition chain C := {in C &, total R}. + +Definition wo_chain C := {in <= C, well_order}. + +Lemma antisymmetric_wo_chain C : + {in C &, antisymmetric R} -> + {in <= C, forall A, nonempty A -> exists z, minimum_of A z} -> + wo_chain C. +Proof. +move=> Ranti Rwo A sAC /Rwo[//|z [Az lbAz]]; exists z; split=> // x [Ax lbAx]. +by apply: Ranti; rewrite ?sAC ?lbAx ?lbAz. +Qed. + +Lemma antisymmetric_well_order : + antisymmetric R -> (forall A, nonempty A -> exists z, minimum_of A z) -> + well_order. +Proof. +by move=> Ranti /withinW/(antisymmetric_wo_chain (in2W Ranti))/withinT. +Qed. + +End RelDefs. + +Lemma wo_chainW (T : eqType) R C : @wo_chain T R C -> chain R C. +Proof. +have ne_cons x s: nonempty [mem x :: s : seq T] by exists x; apply: mem_head. +have all_mem s: all [mem s : seq T] s by apply/allP. +move=> Rwo x y Cx Cy; have /Rwo[] := ne_cons x [::y]; first exact/allP/and3P. +by move=> z [] [] /or3P[] // /eqP-> /allP/and3P[] => [_|] ->; rewrite ?orbT. +Qed. + +Lemma wo_chain_reflexive (T : eqType) R C : @wo_chain T R C -> {in C, reflexive R}. +Proof. by move/wo_chainW => Rtotal x xC; rewrite -[R x x]orbb Rtotal. Qed. + +Lemma wo_chain_antisymmetric (T : eqType) R C : @wo_chain T R C -> {in C &, antisymmetric R}. +Proof. +have ne_cons x s: nonempty [mem x :: s : seq T] by exists x; apply: mem_head. +have all_mem s: all [mem s : seq T] s by apply/allP. +move/[dup]/wo_chainW => Rtotal /[dup]/wo_chain_reflexive Rxx Rwo x y xC yC. +have /Rwo[] := ne_cons x [::y]; first exact/allP/and3P. +move=> z [_ Uz] /andP[Rxy Ryx]; have /and3P[xy_x xy_y _] := all_mem [:: x; y]. +by rewrite -(Uz x) ?(Uz y); split=> //; apply/allP; rewrite /= (Rxy, Ryx) Rxx. +Qed. + +(******************************************************************************) + +Section Zorn. + +Lemma Zorn's_lemma (T : eqType) (R : rel T) (S : {pred T}) : + {in S, reflexive R} -> {in S & &, transitive R} -> + {in <= S, forall C, wo_chain R C -> exists2 z, z \in S & upper_bound R C z} -> + {z : T | z \in S & {in S, maximal R z}}. +Proof. +suffices{T R S} Zorn (T : eqType) (R : rel T) (Well := wo_chain R) : + preorder R -> (forall C, Well C -> {z | upper_bound R C z}) -> + {z | maximal R z}. +- move=> Rxx Rtr UBch; pose T1 := {x | x \in S}. + have S_T1 (u : T1): val u \in S by case: u. + have [|C1 chC1|u maxT1u] := Zorn T1 (relpre val R); last 1 first. + - by exists (val u) => // x Sx Rux; apply: (maxT1u (Sub x Sx)). + - by split=> [x|y x z]; [apply: Rxx | apply: Rtr]. + pose C := [pred x | oapp (mem C1) false (insub x)]. + have sC1C u: u \in C1 -> val u \in C by rewrite inE valK. + have memC x: x \in C -> {u | u \in C1 & val u = x}. + by rewrite inE; case: insubP => //= u _ <-; exists u. + apply/cid; suffices /UBch[_ /memC[u _ <-]//|z Sz ubCz]: wo_chain R C. + by exists (Sub z Sz) => u C1u; apply/ubCz/sC1C. + move=> A sAC [x0 Ax0]. + have [||w [[C1w minC1w] Uw]] := chC1 [preim val of A]. + - by move=> v /sAC; rewrite inE valK. + - by have /sAC/memC[u0 C1u0 Du0] := Ax0; exists u0; rewrite inE Du0. + exists (val w); do ?[split] => // [y Ay | y [Ay minAy]]. + by case/sAC/memC: Ay (Ay) => v C1v <-; apply: minC1w. + have /sAC/memC[v C1v Dv] := Ay; rewrite (Uw v) //. + by split=> [|u Au]; rewrite ?inE /= Dv // minAy. +case=> Rxx Rtr UBch; absurd_not=> nomaxR. +pose R' := [rel x y | R x y && ~~ R y x]. +have{nomaxR} /all_sig[f fP] C: {z | Well C -> upper_bound R' C z}. + have /UBch[z0 _]: Well pred0 by move=> A sA0 [x /sA0]. + have [/UBch[y RCy]|] := asboolP (Well C); last by exists z0. + have [z Ryz notRzy] := nomaxR y; exists z => _ x /RCy-Rxy /=. + by rewrite (Rtr y) //=; contra: notRzy => /Rtr->. +have notCf C: Well C -> f C \notin C. + by move/fP=> R'Cf; apply/negP=> /R'Cf/=; rewrite Rxx ?andbF. +pose f_ind X := Well X /\ {in X, forall x, f [pred y in X | ~~ R x y] = x}. +pose init_seg (X Y : {pred T}) := + {subset X <= Y} /\ {in Y, forall y, y \notin X -> upper_bound R X y}. +have init_total Y Z: f_ind Y -> f_ind Z -> {init_seg Y Z} + {init_seg Z Y}. + move=> indY indZ; pose iniYZ X := `[< init_seg X Y /\ init_seg X Z >]. + pose I x := `[< exists2 X, X \in iniYZ & x \in X >]; pose I1 := [predU1 f I & I]. + have [iIY iIZ]: init_seg I Y /\ init_seg I Z. + split; split=> [x /asboolP[X /asboolP[[sXY _] [sXZ _]]]|]; try by move: (x). + move=> y Yy /asboolP-I'y x /asboolP[X iXYZ Xx]; have /asboolP[[_ RXY] _] := iXYZ. + by rewrite RXY //; contra: I'y; exists X. + move=> z Zz /asboolP-I'z x /asboolP[X iXYZ Xx]; have /asboolP[_ [_ RXZ]] := iXYZ. + by rewrite RXZ //; contra: I'z; exists X. + have maxI: {in iniYZ, forall X, {subset X <= I}}; last clearbody I. + by move=> X sXYZ x Xx; apply/asboolP; exists X. + have Ich: Well I by have [Ych _] := indY; apply: sub_within Ych; case: iIY. + generally have iI1, iI1Y: Y indY iIY {iniYZ maxI} / {I = Y} + {init_seg I1 Y}. + have [[Ych fY] [sIY RIY]] := (indY, iIY). + have /wo_chain_antisymmetric RYanti := Ych. + have [sYI | /notP-ltIY] := asboolP {subset Y <= I}; [left | right]. + by apply/funext=> y; apply/idP/idP=> [/sIY | /sYI]. + have{ltIY} /Ych[_ /andP[]//| z [[/andP/=[I'z Yz]]]]: nonempty [predD Y & I]. + by have [y] := ltIY; exists y; apply/andP. + move=> minYz _; suffices Dz: f I = z. + rewrite /I1 Dz; do 2?[split] => // [x /predU1P[->|/sIY] // | y Yy]. + by case/norP=> /= z'y I'y x /predU1P[->|/RIY->//]; apply/minYz/andP. + rewrite -(fY z Yz); congr f; apply/esym/funext=> x /=. + apply/idP/idP=> [/andP[Yx] | Ix]; first by contra=> I'x; apply/minYz/andP. + have Yx := sIY x Ix; rewrite Yx /=; contra: (I'z) => Rzx. + by rewrite (RYanti z x) // Rzx RIY. + case: iI1Y {iI1}(iI1 Z) => [<- _| iI1Y [||<-|iI1Z]//]; [by left | by right |]. + by case/notCf/negP: Ich; apply/(maxI I1); [apply/asboolP|apply/predU1l]. +pose U x := `[< exists2 X, x \in X & f_ind X >]. +have Umax X: f_ind X -> init_seg X U. + move=> indX; split=> [x Xx | y]; first by apply/asboolP; exists X. + case/asboolP=> Y Yy indY notXy x Xx. + by have [[sYX _]|[_ ->//]] := init_total Y X indY indX; rewrite sYX in notXy. +have RUanti: {in U &, antisymmetric R}. + move=> x y /asboolP[X Xx indX] /asboolP[Y Yy indY]. + without loss [sXY _]: x y X Y Xx Yy {indX} indY / init_seg X Y. + move=> IH. + by case: (init_total X Y) => // {}/IH-IH; [|rewrite andbC] => /IH->. + have [/wo_chain_antisymmetric RYanti _] := indY. + by apply: RYanti => //; apply: sXY. +have Uch: Well U. + apply: antisymmetric_wo_chain => // A sAU [x0 Ax0]. + have /sAU/asboolP[X Xx0 indX] := Ax0. + pose B := [predI A & X]; have sBX: {subset B <= X} by move=> y /andP[]. + have [[Xch _] /Umax[sXU iXU]] := (indX, indX). + have{x0 Ax0 Xx0} /Xch[//|z [[/andP[/= Az Xz] minBz] _]]: nonempty B. + by exists x0; apply/andP. + exists z; split=> // y Ay; have Uy := sAU y Ay. + by have [Xy | /iXU->//] := boolP (y \in X); apply/minBz/andP. +pose U1 := [predU1 f U & U]; have notUfU: f U \notin U by apply: notCf. +suffices indU1: f_ind U1. + by have [sU1U _] := Umax U1 indU1; rewrite sU1U ?inE ?eqxx in notUfU. +have RU1fU: upper_bound R U1 (f U) by move=> x /predU1P[-> // | /fP/andP[]] . +split=> [A sAU1 neA | x U1x]. + have [sAfU | {neA}/notP[x Ax fU'x]] := asboolP {subset A <= pred1 (f U)}. + have AfU: f U \in A by have [x Ax] := neA; have /sAfU/eqP<- := Ax. + by exists (f U); split=> [|y [/sAfU/eqP//]]; split=> // _ /sAfU/eqP->. + have Ux: x \in U by case/sAU1/orP: Ax => // /idPn. + pose B := [predI A & U]; have sBU: {subset B <= U} by move=> y /andP[]. + have /Uch[//|z [[/andP[/= Az Uz] minBz] _]]: nonempty B. + by exists x; apply/andP. + have{minBz} minAz: lower_bound R A z. + move=> y Ay; case/sAU1/predU1P: (Ay) => [->|/= Uy]; first exact/RU1fU/sAU1. + exact/minBz/andP. + exists z; do ?[split] => // y [Ay minAy]. + have /sAU1/predU1P[Dy|Uy] := Ay; last by apply: RUanti; rewrite ?minAz ?minAy. + by have /andP[_] := fP U Uch z Uz; rewrite -Dy minAy. +have /predU1P[-> | /asboolP[X Xx indX]] := U1x. + congr f; apply/funext=> y; apply/idP/idP=> [|Uy]; last first. + by rewrite !inE unfold_in -/(U y) Uy orbT; case/andP: (fP U Uch y Uy). + by case/andP=> /predU1P[->|//]; rewrite Rxx. +have{indX} [[_ f_indX] /Umax[sXU iXU]] := (indX, indX). +rewrite -[RHS]f_indX //; congr f; apply/funext=> y; apply/andb_id2r=> notRyx. +apply/idP/idP=> [U1y | Xy]; last exact/predU1r/sXU. +by contra: notRyx => notXy; have /predU1P[->|/iXU->] := U1y; first apply/RU1fU. +Qed. + +Theorem Hausdorff_maximal_principle T R (S C : {pred T}) : + {in S, reflexive R} -> {in S & &, transitive R} -> chain R C -> {subset C <= S} -> + {M : {pred T} | + [/\ {subset C <= M}, {subset M <= S} + & forall X, chain R X -> {subset M <= X} -> {subset X <= S} -> M = X]}. +Proof. +move=> Rxx Rtr Cch sCS. +pose CSch X := `[< [/\ chain R X, {subset C <= X} & {subset X <= S}] >]. +pose Rch (X Y : {pred T}) := `[< {subset X <= Y} >]. +have: {in CSch & &, transitive Rch}. + by apply: in3W => X Y Z /asboolP-sXY /asboolP-sYZ; apply/asboolP=> x /sXY/sYZ. +have /Zorn's_lemma/[apply]: {in CSch, reflexive Rch} by move=> X _; apply/asboolP. +case=> [XX CSchXX XXwo | M /asboolP[Mch sCM sMS] maxM]; last first. + exists M; split=> // X Xch sMX sXS. + suffices /asboolP-sXM: Rch X M by apply/funext=> x; apply/idP/idP=> [/sMX|/sXM]. + by apply: maxM; apply/asboolP=> //; split=> // x /sCM/sMX. +move/(@wo_chainW {pred T}): XXwo => XXch. +without loss XX_C: XX CSchXX XXch / C \in XX. + have CSchC: C \in CSch by apply/asboolP; split. + have RchC_CSch X: X \in CSch -> Rch C X by case/asboolP=> _ sCX _; apply/asboolP. + pose XX1 X := `[< X = C \/ X \in XX >]. + have CSchXX1: {subset XX1 <= CSch} by move=> X /asboolP[-> | /CSchXX]. + case/(_ XX1)=> // [||Z CSchZ ubZ]; first 2 [by apply/asboolP; left]. + move=> X Y /asboolP[-> /CSchXX1/RchC_CSch-> //| XX_X]. + by rewrite orbC => /asboolP[-> | /XXch->//]; rewrite RchC_CSch ?CSchXX. + by exists Z => // X XX_X; apply/ubZ/asboolP; right. +pose D x := `[< exists2 X, X \in XX & x \in X >]. +have sCD: {subset C <= D} by move=> x Cx; apply/asboolP; exists C. +have sDS: {subset D <= S} by move=> x /asboolP[X /CSchXX/asboolP[_ _ sXS] /sXS]. +have in2D: {in D &, forall x y, exists X, [/\ X \in XX, x \in X & y \in X]}. + move=> x y /asboolP[X XX_X Xx] /asboolP[Y XX_Y Yy]; have:= XXch X Y XX_X XX_Y. + by case/orP=> [/asboolP/(_ x Xx)|/asboolP/(_ y Yy)]; [exists Y | exists X]. +exists D => [|X XX_X]; last by apply/asboolP=> x Xx; apply/asboolP; exists X. +apply/asboolP; split=> //. +move=> x y xD /(in2D x)-/(_ xD) [X [/CSchXX/asboolP[Xch _ _] Xx Xy]]. +exact: Xch. +Qed. + +Theorem well_ordering_principle (T : eqType) : {R : rel T | well_order R}. +Proof. +have{T} [T ->]: {T1 : eqType | T = T1} by exists T. +pose srel := pred T * rel T : Type. +pose loc (R : srel) := [rel x y | [&& x \in R.1, y \in R.1 & R.2 x y]]. +pose pwo (R : srel) := `[< wo_chain R.2 R.1 >]. +pose init_seg (R S : srel) := + {in R.1 & S.1, forall x y, S.2 x y = (y \in R.1) ==> R.2 x y}. +pose initR R S := `[< {subset R.1 <= S.1} /\ init_seg R S >]. +have initRR: reflexive initR by move=> R; apply/asboolP; split=> // x y _ ->. +have initRtr: transitive initR. + move=> R2 R1 R3 /asboolP[D12 R12] /asboolP[D23 R23]; apply/asboolP. + split=> [x /D12/D23// | x y D1x D3y]; rewrite R23 ?(D12 x) //. + by case D2y: (y \in R2.1); [apply: R12 | rewrite (contraFF (D12 y))]. +have: {in pwo & &, transitive initR} by apply: in3W. +have/Zorn's_lemma/[apply]: {in pwo, reflexive initR} by []. +case=> [C pwoC Cch | [D R] /asboolP/=pwoR maxR]. + have /(@wo_chainW ({pred T} * rel T)%type) {}Cch := Cch. + pose D x := `[< exists2 S, S \in C & x \in S.1 >]; pose R x y := `[< exists2 S, S \in C & loc S x y >]. + exists (D, R). + apply/asboolP=> /= X sXD [x Xx]; have /sXD/asboolP[R0 CR0 /= D0x] := Xx. + have /pwoC/asboolP/=R0wo := CR0. + have{x Xx D0x}: nonempty [predI X & R0.1] by exists x; apply/andP. + case/R0wo=> [_ /andP[]// |z [[/andP/=[Xz D0z] min0z] _]]. + have{R0 CR0 R0wo D0z min0z} minXz: lower_bound R X z. + move=> y Xy; have /sXD/asboolP[R1 /= CR1 D1y] := Xy. + have /orP[/asboolP/=[D10 R10] | /asboolP/=[D01 R01]] := Cch _ _ CR1 CR0. + by apply/asboolP; exists R0; rewrite //= D0z min0z ?inE ?Xy D10. + apply/asboolP; exists R1; rewrite //= R01 ?D1y// D01//=. + by apply/implyP=> D0y; apply/min0z/andP. + exists z; split=> // y [{}/minXz/asboolP[R0 CR0 R0zy] minXy]. + case/minXy/asboolP: Xz => {minXy} R1 CR1 R1yz. + without loss /asboolP[D01 R01]: y z R0 R1 CR0 CR1 R0zy R1yz / initR R0 R1. + by move=> IH; have /orP[/(IH y z)-> | /(IH z y)-> ] := Cch _ _ CR0 CR1. + have{R1yz R0zy} [/and3P[D1y D1z R1zy] /and3P[D0z D0y R0yz]] := (R1yz, R0zy). + have /pwoC/asboolP/wo_chain_antisymmetric R1anti := CR1. + by apply: R1anti => //; rewrite R1zy R01 // D0y R0yz. + move=> R0 CR0; apply/asboolP; split=> [x D0x|]; first by apply/asboolP; exists R0. + move=> x y D0x Dy; apply/asboolP/idP=> [[R1 CR1 /and3P[D1x D1y R1xy]] | R0xy]. + have /orP[/asboolP[_ R10] | /asboolP[_ <- //]] := Cch _ _ CR1 CR0. + by apply/implyP=> D0y; rewrite R10 // D1y R1xy. + case/asboolP: Dy => R1 CR1 D1y. + have /orP[/asboolP[D10 _] | /asboolP[D01 R01]] := Cch _ _ CR1 CR0. + by exists R0; rewrite //= D0x (implyP R0xy) D10. + by exists R1; rewrite //= D1y D01 ?R01. +exists R; apply: withinT; apply: sub_within (pwoR) => z _; assume_not=> notDz. +pose Rz x := predU1 z (if x \in D then R x else pred0). +have /maxR/(_ _)/asboolP: ([predU1 z & D] : pred T, Rz : rel T) \in pwo. + apply/asboolP=> X sXxD neX; pose XD := [predI X & D]. + have [{neX}/pwoR[_ /andP[]//|x] | sXz] := asboolP (nonempty XD); last first. + have {}sXz x: x \in X -> x = z. + move=> Xx; case/sXxD/predU1P: (Xx) => // Dx. + by case: sXz; exists x; apply/andP. + have [x Xx] := neX; exists x; have /sXz-eq_xz := Xx. + by split=> [|_ [/sXz-> //]]; split=> // _ /sXz->; apply/predU1l. + case=> -[/andP/=[Xx Dx] minXDx] Ux; exists x; split=> [|y [Xy minXy]]. + split=> // y Xy; have /sXxD/predU1P[-> | Dy] := Xy; first exact/predU1l. + by rewrite /= Dx; apply/predU1r/minXDx/andP. + have Dy: y \in D. + have /minXy/= := Xx; case: ifP => // _ /idPn[]. + by rewrite negb_or andbT (memPn notDz). + apply: Ux; split=> [|t /andP[/minXy]]; first exact/andP. + by rewrite /= Dy => /predU1P[-> /idPn[]|]. +case=> [|/= -> //]; last exact/predU1l. +apply/asboolP; split=> [x|x y /= Dx]; first exact: predU1r. +rewrite Dx => /predU1P[-> | /= Dy]; first by rewrite eqxx (negPf notDz). +by rewrite Dy -implyNb (memPn notDz). +Qed. + +End Zorn.