proposition: Lemma Exercise4_10d E n (F := (fun_image E singleton) \cup (fun_image E (fun z => E -s1 z))) (r := sub_order F): natp n -> cardinal E = n -> ( Ex4_10_hyp r n /\ forall m, natp m -> Ex4_10_hyp r m -> n <=c m).
proof: Proof. move=> nN cen. move:(sub_osr F) => [or sr]. case: (equal_or_not n \0c) => nz. split; last by move=> m mb _; rewrite nz; apply: cle0n. set g := Lg emptyset id. have pa: order_fam g by rewrite /g;hnf;aw;move => t /in_set0. move: (order_product_osr pa) => [pb pb']. move: empty_function_function => [pc pd pe]. have bef: bijection empty_function. split; split => //; rewrite pd ?pe; [move => x y | move => y]; case; case. exists g, emptyset, empty_function; rewrite/g;saw. by hnf;aw;move => t /in_set0. by rewrite cardinal_set0. fprops. have hh: sub emptyset (substrate (order_product g)) by fprops. move: (iorder_osr pb hh)=> [sa sb]. split => //. rewrite sb; split => //; rewrite pd sr /F. rewrite nz in cen; move: (card_nonempty cen) => ->. by rewrite funI_set0 funI_set0 setU2_id. by hnf; rewrite pd; move => x y /in_set0. have pa: forall a, inc a E -> inc (singleton a) F. move => a ae; apply /setU2_P; left; apply /funI_P; ex_tac. have pb: forall a, inc a E -> inc (E -s1 a) F. move => a ae; apply /setU2_P; right; apply /funI_P; ex_tac. have pc: forall a b, inc a E -> inc b E -> a <> b -> gle r (singleton a) (E -s1 b). move => a b aE bE and; apply /sub_gleP;split;fprops. move => t /set1_P ->; apply /setC1_P;split => //. have pd: forall a, inc a E -> singleton a <> E -s1 a. by move => a ae eq; move: (set1_1 a); rewrite eq;apply /setC1_P => //; case. split. set F1:= fun_image E singleton. pose ra x := (union x). pose rb x := (union (E -s x)). have splitF: forall x, inc x F -> ( [/\ inc x F1, inc (ra x) E & x = singleton (ra x)] \/ [/\ inc x (F -s F1), inc (rb x) E & x = E -s1 (rb x)]). move => x; rewrite /F -/F1 /ra /rb => xF. case: (inc_or_not x F1) => xF1. by left; move: (xF1) => /funI_P [z zE h]; rewrite {2 4} h !setU_1. right;move: (xF) => /setU2_P; case => //; move /funI_P => [z zE zv]. set t := (E -s x). have ->: t = singleton z by rewrite /t zv setC_K // => q /set1_P ->. by rewrite setU_1; split => //; apply /setC_P. apply (Exercise4_10b or nN nz). have [h [bh sh th]]: exists h, bijection_prop h (Nint n) E. by apply /card_eqP; rewrite card_Nint. move: (Nintco_wor n) => []. set rI := Nint_co n; move => worI srI. pose hk k := (h \co shift_mod_n n k). have bcs: forall k, k<c n -> substrate rI = source (hk k). by move => k kn; rewrite /hk /shift_mod_n; aw. have bcp: forall k, k<c n -> (h \coP shift_mod_n n k /\ bijection (hk k)). move => k kn. move: (shift_mod_n_fb nN nz kn) => bs. have qb: h \coP shift_mod_n n k. by split => //; try fct_tac; rewrite /shift_mod_n; aw. by split => //; apply: compose_fb. have F1F: sub F1 F by move => t ta; apply /setU2_P; left. pose hi k x := Vf (inverse_fun (hk k)) x. have bce: forall k x, k <c n -> inc x E -> inc (hi k x) (substrate rI). move => k x kn xE. move: (bcp _ kn) => [_ bk]. move: (inverse_bij_fb bk) =>[[fik _] _]. have si: source (inverse_fun (hk k)) = E by aw; rewrite /hk; aw. have -> : substrate rI = target (inverse_fun (hk k)) by aw; rewrite - bcs. rewrite /hi;Wtac. have bcf:forall k x y, k <c n -> inc x E -> inc y E ->hi k x = hi k y -> x= y. move => k x y kn. move: (bcp _ kn) => [_ bk]. have <- : target (hk k) = E by rewrite /hk; aw. move => xE yE sv; move : (f_equal (fun z => Vf (hk k) z) sv). rewrite inverse_V // inverse_V //. move: (worI) => [orI _]. move: (worder_total worI) => [_ torI]. pose r1 k x y := [\/ [/\ inc x F1, inc y F1 & (gle rI (hi k (ra x)) (hi k (ra y)))], [/\ inc x F1, inc y (F -s F1) & (ra x <> rb y \/ (ra x = rb y /\ (hi k (ra x) <> cpred n)))], [/\ inc x (F -s F1), inc y F1, (rb x = ra y) & (hi k (ra y)) = cpred n ] | [/\ inc x (F -s F1), inc y (F -s F1) & (gle rI (hi k (rb y)) (hi k (rb x)))]]. have dr1: forall k x y, r1 k x y -> (inc x F /\ inc y F). move => k x y; case. by move => [qa qb _]; split => //; apply: F1F. by move => [qa] /setC_P [yf _] _;split => //;apply: F1F. by move => [] /setC_P [xa _] yb _;split => //;apply: F1F. by move => [] /setC_P [xa _] /setC_P [ya _] _;split => //. have dr2: forall k x, k <c n -> inc x F -> r1 k x x. move => k x kn xF. case: (splitF _ xF); move => [qa qb qc]. by constructor 1; split => //; order_tac;apply: bce. by constructor 4; split => //; order_tac; apply: bce. have dr3: forall k x y, k <c n -> inc x F -> inc y F -> r1 k x y \/ r1 k y x. move => k x y kn xF yF. case: (splitF _ xF) =>[] [qa qb qc]; case: (splitF _ yF)=> [] [qd qe qf]. - move: (bce _ _ kn qb) (bce _ _ kn qe) => sr1 sr2. by case: (torI _ _ sr1 sr2); [left | right ]; in_TP4. - case: (equal_or_not (ra x) (rb y)) => cpi. case: (equal_or_not (hi k (ra x)) (cpred n)) => cpj. right;in_TP4. by left; constructor 2; split => //; right. by left; constructor 2; split => //; left. - case: (equal_or_not (ra y) (rb x)) => cpi. case: (equal_or_not (hi k (ra y)) (cpred n)) => cpj. left; in_TP4. by right; constructor 2;split => //; right. by right; constructor 2;split => //; left. - move: (bce _ _ kn qb) (bce _ _ kn qe) => sr1 sr2. by case: (torI _ _ sr2 sr1); [left | right ]; in_TP4. have dr4: forall k x y, k<c n -> r1 k x y -> r1 k y x -> x = y. move => k x y kn c1 c2. move: (dr1 _ _ _ c1) => [xF yF]; case: c1. - move => [xF1 yF1 le1]. have sa: inc x (F -s F1) -> False by move /setC_P => []. have sb: inc y (F -s F1) -> False by move /setC_P => []. case: (splitF _ xF); last by move => []. case: (splitF _ yF); last by move => []. move => [_ qb qc] [_ qb' qc']. case: c2; [ | move => [] | move => [] | move => []] => //. move => [_ _ le2]. have eq1: (hi k (ra y)) = (hi k (ra x)) by order_tac. by rewrite qc qc' (bcf _ _ _ kn qb qb' eq1). - move => [xF1 yF1 le1]. have sa: inc x (F -s F1) -> False by move /setC_P => []. move: (yF1) => /setC_P [_ sb]. case: c2; [ move => [] | move => [] | | move => [_ ]] => //. move => [_ _ ta tb]. by case: le1; rewrite ta //; move => []. - move => [xF1 yF1 ta tb]. have sa: inc y (F -s F1) -> False by move => /setC_P []. move: (xF1); move => /setC_P [_ sb]. case: c2; [ move => [] | | move => [] | move => [] ] => //. by move => [_ _]; rewrite ta;case => //; move => []. - move => [xF1 yF1 le1]. move: (xF1)(yF1) =>/setC_P [_ sa] /setC_P [_ sb]. case: c2; [move => [] | move => [] | move =>[] | move=> [_ _ le2]] => //. have eq1: (hi k (rb y)) = (hi k (rb x)) by order_tac. case: (splitF _ xF); first by move => []. case: (splitF _ yF); first by move => []. move => [_ qb ->] [_ qb' ->]. by rewrite (bcf _ _ _ kn qb qb' eq1). move: (cpred_pr nN nz); move=> [pnN pnv]. have lcpnn: cpred n <c n by rewrite {2} pnv; apply: cltS. have QA: forall u v, gle rI u v -> u = v \/ u <c cpred n. move => u v le1; case: (equal_or_not u v); [by left | move => uv; right]. move: le1 => /(Nintco_gleP nN) [luv vn]. move: vn; rewrite {1} pnv; move / (cltSleP pnN) => tc. exact (clt_leT (conj luv uv) tc). have QB: forall u, inc u (substrate rI) -> gle rI u (cpred n). move => u; rewrite srI => /(NintP nN) uc. apply /(Nintco_gleP nN);split => //. by move: uc; rewrite {1} pnv;move /(cltSleP pnN). have dr5: forall k x y z, k<c n -> r1 k x y -> r1 k y z -> r1 k x z. move => k x y z kn le1 le2. move: (dr1 _ _ _ le1) (dr1 _ _ _ le2) => [xF yF] [_ zF]. case: le1. - move => [xF1 yF1 le1]. have sa: inc x (F -s F1) -> False by move /setC_P => []. have sb: inc y (F -s F1) -> False by move /setC_P => []. case: (splitF _ xF); last by move => []. case: (splitF _ yF); last by move => []. move => [_ qb qc] [_ qb' qc']. case: le2; move => [p1 p2 p3] => //. constructor 1;split => //; order_tac. constructor 2; split => //. case: (equal_or_not (ra x) (ra y)); [ by move => -> | move => nexy]. case: (equal_or_not (ra x) (rb z)) => eq1; last by left. right; case: (equal_or_not (hi k (ra x)) (cpred n)) => e2; last by done. case:(QA _ _ le1); first by move => tb; move: (bcf _ _ _ kn qb' qb tb). by move => [_ neq]. - move => [xF1 yF1 le1]; move: yF1 => /setC_P [_ nyF1]. case: le2; move=> [p1 p2 p3] //. move => p4; constructor 1 ;split => //; rewrite p4; apply: QB. apply: bce => //; case: (splitF _ xF); move => [ta tb _] //. by move: ta => /setC_P [_ bad]. constructor 2; split => //. case: (equal_or_not (rb y) (rb z)); [ by move => <- | move => neyz]. case: (equal_or_not (ra x) (rb z)) => eq1; last by left. right; case: (equal_or_not (hi k (ra x)) (cpred n)) => e2 //. case: (QA _ _ p3); last by rewrite -eq1; move => [_ aux];split => //. move => tb; case: neyz. case: (splitF _ yF); [by move => [] | move => [_ qb' qc']]. case: (splitF _ zF); [move => [zf1 _] | move => [_ qb qc]]. by move: p2 => /setC_P []. by rewrite (bcf _ _ _ kn qb qb' tb). - move=> [xF1 yF1 eq1 eq2]; move: (xF1) => /setC_P [_ nxF1]. have tc: inc y (F -s F1) -> False by move /setC_P => []. case: le2; move=> [p1 p2 p3] //. case: (QA _ _ p3); last by move => [_]. case: (splitF _ yF); last by move => []. case: (splitF _ zF); last by move => [bad _]; move: bad => /setC_P []. move => [_ qb qc] [_ qb' qc'] tb. move: (bcf _ _ _ kn qb' qb tb) => sra. constructor 3;split => //; ue. constructor 4; split => //. rewrite eq1 eq2;apply: QB; apply: bce => //. case: (splitF _ zF); last by move => [_ ok _]. by move: p2 => /setC_P [_ qa] [qb _]. - move => [xF1 yF1 le1]. have sa: inc x F1 -> False by move: xF1 => /setC_P []. have sb: inc y F1 -> False by move: yF1 => /setC_P []. case: (splitF _ xF); first by move => []. case: (splitF _ yF); first by move => []. move => [_ qb qc] [_ qb' qc']. case: le2; move => [p1 p2 p3] //. move => p4; constructor 3;rewrite p3 in le1. case: (QA _ _ le1); last by move=> [_ h0]. case: (splitF _ zF); move => [ta tb tc]. move => le4; rewrite - (bcf _ _ _ kn tb qb' le4);split => //. by move: ta => /setC_P []. constructor 4;split => //; order_tac. pose ork k := (graph_on (r1 k) F). have dr6: forall k, k <c n -> (total_order (ork k) /\ substrate (ork k) = F). move => k kn. have srk: substrate (ork k) = F. by rewrite /ork graph_on_sr // => a; apply: dr2. split; [split | by exact]. apply: order_from_rel; split => //. by move => x y z; apply: dr5. by move => x y ; apply: dr4. by move => x y xy; move: (dr1 _ _ _ xy) => [xE yE];split; apply: dr2. by rewrite srk => x y xE yE; move: (dr3 _ _ _ kn xE yE); case => au; [left | right ]; apply /graph_on_P1. have dr7: forall k x y, k <c n -> gle r x y -> gle (ork k) x y. move => k x y kn. move: (dr6 _ kn) => [[ori _] sri]. move /sub_gleP => [xF yF sxy]. case: (equal_or_not x y) => exy; first by rewrite -exy; order_tac; ue. apply /graph_on_P1; split => //. case: (splitF _ xF); case: (splitF _ yF);move => [yF1 ry ys] [xF1 rx xs]. - move: (set1_1 (ra x)); rewrite -xs =>h0; move: (sxy _ h0). by rewrite ys => /set1_P => h1; case: exy; rewrite xs ys h1. - constructor 2;split => //; left; move => h1. move: (set1_1 (ra x)); rewrite -xs =>h0; move: (sxy _ h0). by rewrite ys => /setC_P [_] /set1_P. - case: (equal_or_not (rb x) (ra y)) => ns; last first. case: exy; apply: extensionality =>//. rewrite ys xs; move => z /set1_P ->; apply /setC_P. by split => // /set1_P; apply: nesym. have Es: E = singleton (rb x). apply: set1_pr => // z zE; ex_middle zb. have zx: inc z x by rewrite xs; apply/setC_P;split => //; move /set1_P. move: (sxy _ zx); rewrite ys -ns; move /set1_P => //. have n1: n = \1c by rewrite - cen Es cardinal_set1. constructor 3;split => //. move: (bce _ _ kn ry); rewrite srI; move /(NintP nN). by rewrite n1; move /clt1; rewrite - succ_zero (cpred_pr2 NS0). - case: exy; rewrite xs ys; congr (E -s1 _). case: (p_or_not_p (inc (rb y) x)) => h1. by move: (sxy _ h1); rewrite {2} ys => /setC_P [_] /set1_P. move: h1; rewrite {1}xs => /setC_P aux; ex_middle ok;case:aux;split => //. by move /set1_P; apply:nesym. have zz : \0c <c n by apply /strict_pos_P1. have zn: inc \0c (Nint n) by apply /NintP. have zd: inc \0c (domain (Lg (Nint n) ork)) by aw. case: (emptyset_dichot (Lg (Nint n) ork)) => lne. have : inc (J \0c (ork \0c)) (Lg (Nint n) ork). by apply /funI_P; ex_tac. by rewrite lne; move /in_set0. have hii: forall x, inc x E -> exists2 k, k<c n & hi k x = cpred n. move => x xE; move: (xE); rewrite -th => xE1. move: (bij_surj bh xE1) => [y ys yv]. move: ys; rewrite sh => /(NintP nN) yn. have cpin: inc (cpred n) (Nint n) by apply /NintP. set k := Yo (y = cpred n) \0c (csucc y). move: (NS_le_nat (proj1 yn) nN) => yN. have kn: k <c n. rewrite /k; Ytac cyn => //. rewrite pnv; apply /(cltSleP pnN). apply /(cleSltP yN); split => //. by apply /(cltSleP pnN); ue. have srhk: (source (hk k)) = (Nint n) by rewrite /hk/shift_mod_n; aw. have cpsh: inc (cpred n) (source (hk k)) by rewrite srhk. have qh: inc (hi k x) (source (hk k)). by move: (bce _ _ kn xE); rewrite srI srhk. move: (bcp _ kn) => [ta tb]. have tc: inc (cpred n) (source (shift_mod_n n k)). by rewrite /shift_mod_n; aw. move: (shift_mod_n_ax nN nz (NS_le_nat (proj1 kn) nN)) => td. have xv1: x = Vf (hk k) (cpred n). rewrite /hk compfV// /shift_mod_n LfV// shift_mod_n_vl //. rewrite /k; case: (equal_or_not y (cpred n)) => yp; Ytac0. by rewrite (csum0r (CS_nat pnN)); Ytac0; rewrite -yp. have ->: cpred n +c csucc y = n +c y. by rewrite (csum_nS _ yN) - (csum_Sn _ pnN) -pnv. rewrite (Y_false (cleNgt (Nsum_M0le y nN))). by rewrite csumC cdiff_pr1. have xt: inc x (target (hk k)) by rewrite xv1; Wtac; fct_tac. exists k=> //; apply: (bij_inj tb qh cpsh). by rewrite /hi -/k (inverse_V tb xt). have hij: forall x, inc x E -> exists2 k, k<c n & hi k x = \0c. move => x xE; move: (xE); rewrite -th => xE1. move: (bij_surj bh xE1) => [y ys yv]. move: ys; rewrite sh => /(NintP nN) yn. exists y => //. have srhk: (source (hk y)) = (Nint n) by rewrite /hk/shift_mod_n; aw. have cpsh: inc \0c (source (hk y)) by rewrite srhk. have qh: inc (hi y x) (source (hk y)) by move: (bce _ _ yn xE); rewrite srI srhk. move: (bcp _ yn) => [ta tb]. have tc: inc \0c (source (shift_mod_n n y)) by rewrite /shift_mod_n; aw. move: (shift_mod_n_ax nN nz (NS_le_nat (proj1 yn) nN)) => td. have xv1: x = Vf (hk y) \0c. rewrite /hk compfV// /shift_mod_n (LfV td zn). rewrite shift_mod_n_vl // (csum0l (proj31_1 yn)); Ytac0; ue. have xt: inc x (target (hk y)) by rewrite xv1; Wtac; fct_tac. apply: (bij_inj tb qh cpsh). by rewrite /hi (inverse_V tb xt). have dr8: r = intersectionb (Lg (Nint n) ork). set_extens t => te. have gr: sgraph r by fprops. move: (gr _ te); rewrite /pairp; set x := P t; set y := Q t => pt. apply: (setIb_i lne); aw => i idn; rewrite LgV//. move: idn => /(NintP nN) => idn. move: te; rewrite -pt -/(related r x y) -/(gle r x y). rewrite -/(related (ork i) x y) -/(gle (ork i) x y). by apply: dr7. move: lne => [xc xcb]; move: (setIb_hi te zd); rewrite LgV// => toz. move: (dr6 _ zz); move=> [[orz _] srz]. have grz: sgraph (ork \0c) by fprops. move: (grz _ toz); rewrite /pairp; set x := P t; set y := Q t => pt. rewrite -pt -/(related r x y) -/(gle r x y). have aux1: forall k, k <c n -> gle (ork k) x y. move => k kn. have kd: inc k (Nint n) by apply /(NintP nN). have kd1: inc k (domain (Lg (Nint n) ork)) by aw. move: (setIb_hi te kd1); rewrite LgV// - pt //. have aux: forall k, k <c n -> r1 k x y. by move => k kn; move: (aux1 _ kn) => /graph_on_P1 [_ _ ]. move: (aux1 _ zz) => le1. have xF: inc x F by rewrite - srz; order_tac. have yF: inc y F by rewrite - srz; order_tac. clear xcb toz orz grz le1. apply /sub_gleP;split => //. case: (splitF _ xF); case: (splitF _ yF); move => [yF1 ry ys] [xF1 rx xs]. case: (equal_or_not (ra x) (ra y)) => nsv. rewrite xs ys nsv; fprops. have b1: inc y (F -s F1) -> False by move /setC_P => []. have b2: inc x (F -s F1) -> False by move /setC_P => []. move: (hii _ rx) => [k kn hl]. case: (aux _ kn) => [] [p1 p2 p3] //. case: (QA _ _ p3) => ww; last by move: ww => [_]. rewrite ys xs; rewrite (bcf _ _ _ kn rx ry ww); fprops. have b2: inc x (F -s F1) -> False by move /setC_P => []. have b1: inc y F1 -> False by move: yF1; move /setC_P => []. move: (hii _ rx); move => [k kn hl]. case: (aux _ kn) => [][p1 p2 p3] //. case: p3; last by move => [_ ok]. by move => ta; rewrite xs ys /setC1_P => z /set1_P ->; apply /setC1_P. have b2: inc y (F -s F1) -> False by move /setC_P => []. have b1: inc x F1 -> False by move: xF1 => /setC_P []. move: (hij _ ry); move => [k kn hl]. case: (aux _ kn) => [] [p1 p2 p3] //. move=>tb z; rewrite xs => /setC1_P [sa sb]. move: cen; rewrite pnv -tb hl succ_zero => /set_of_card_oneP cen. by move: cen sa rx sb=> [q ->] /set1_P -> /set1_P ->. have b2: inc y F1 -> False by move: yF1 => /setC_P []. have b1: inc x F1 -> False by move: xF1 => /setC_P []. move: (hii _ ry); move => [k kn hl]. case: (aux _ kn) => [] [p1 p2 p3] //. case: (QA _ _ p3) => ww; last by move: ww => [_]. rewrite ys xs; rewrite (bcf _ _ _ kn ry rx ww); fprops. exists (Lg (Nint n) ork); split => //. hnf;move => k kn; rewrite LgV//; move: kn; aw;trivial => /(NintP nN) kn. by move: (dr6 _ kn) ; move => [[ok _] _]. hnf;aw;move =>k kn; rewrite LgV//; move: kn => /(NintP nN) kn. by move: (dr6 _ kn) ; move => [ok _]. by aw; rewrite card_Nint. aw; move => k kn; rewrite LgV//; move: kn => /(NintP nN) kn. by move: (dr6 _ kn) ; move => [_ ->]; rewrite sr. move => m mN h. set F1:= fun_image E singleton. case: (emptyset_dichot E). by move => ee //; case: nz; rewrite - cen ee // cardinal_set0. case: (equal_or_not m \0c) => mz. move => [a aE]; move: (pd _ aE) (pa _ aE) (pb _ aE) => nab aF bF. move: h => [g [A [f [ofg atg cdg asg [_ _ [bf sf tf] _]]]]]. rewrite sr in sf; rewrite - sf in aF bF. case: nab; apply (bij_inj bf aF bF). have ff: function f by fct_tac. move: (Vf_target ff aF) (Vf_target ff bF) => w1 w2. move:(order_product_osr ofg)=> [op sp]. move: (asg); rewrite sp. move: tf; rewrite (iorder_sr op asg) => <- pe. move: (pe _ w1)(pe _ w2) => /prod_of_substratesP [qa qb _] /prod_of_substratesP [qc qd _]. apply: fgraph_exten => //; first by ue. rewrite mz in cdg. by rewrite qb (card_nonempty cdg) => x /in_set0. move => [a aE]. move: (Exercise4_10a or mN mz h) =>[g [ofg atg cdg asi ri]]. have fs1: finite_set F1. by apply: finite_fun_image; hnf; rewrite cen; apply /NatP. have sdf: sub F1 (substrate r) by rewrite sr /F/F1 =>t; fprops. have nef: nonempty F1 by exists (singleton a); apply /funI_P; ex_tac. pose gei i := the_greatest (induced_order (Vg g i) F1). have gei_pr: forall i, inc i (domain g) -> greatest (induced_order (Vg g i) F1) (gei i). move => i idg; move: (atg _ idg) => to1. rewrite -(asi _ idg) in sdf. move: (finite_subset_torder_greatest to1 fs1 nef sdf) => h1. move: (iorder_osr (proj1 to1) sdf)=> [or2 _]. exact (the_greatest_pr or2 h1). pose gej i := union (gei i). have gej_pr: forall i, inc i (domain g) -> (inc (gej i) E /\ singleton (gej i) = gei i). move => i idg; move: (gei_pr _ idg) => [h1 _]. move: (proj1 (atg _ idg)) => o1. rewrite - (asi _ idg) in sdf. move: h1; rewrite iorder_sr //; move /funI_P => [z ze sz]. by rewrite /gej sz setU_1. case: (cleT_el (CS_nat nN) (CS_nat mN)) => // ltmn. move: (fun_image_smaller (domain g) gej). set F2:= fun_image (domain g) gej; rewrite cdg => aux. have ss: ssub F2 E. split. by move => t /funI_P [z zdg ->]; case: (gej_pr _ zdg). move: (cle_ltT aux ltmn). by rewrite - cen; move => [_ h1]; dneg xx; rewrite xx. move: (setC_ne ss) => [xc] /setC_P [xce nxcf2]. have cp1: forall i, inc i (domain g) -> gle (Vg g i) (singleton xc) (E -s1 xc). move => i idg; move: (gej_pr _ idg) (gei_pr _ idg) => [qa qb] []. have scf1: inc (singleton xc) F1 by apply /funI_P; exists xc. move: (ofg _ idg) => oi. rewrite - (asi _ idg) in sdf. rewrite (iorder_sr oi sdf) => [_ gt]. move: (iorder_gle1 (gt _ scf1)) => qc. case: (equal_or_not (gej i) xc) => nexci. case: nxcf2; rewrite - nexci; apply /funI_P; ex_tac. have le1: gle r (gei i) (E -s1 xc) by rewrite -qb; apply: pc. have le2: gle (Vg g i) (gei i) (E -s1 xc). by move: le1; rewrite /gle/related /r ri => le1; apply: setIb_hi. order_tac. case: (emptyset_dichot g) => // ge. by case: mz; rewrite - cdg ge domain_set0 cardinal_set0. have : gle r (singleton xc) (E -s1 xc). rewrite /gle/related /r ri; apply: setIb_i => // i idg. move /sub_gleP => [_ _ hp]. by move: (hp _ (set1_1 xc)) => /setC1_P [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)