proposition: Lemma Exercise2_7A12: exists r u v, [/\ order r, inductive r, inc u (closures r), inc v (closures r) & ~ has_supremum (closure_ordering r) (doubleton u v)].
proof: Proof. move: Exercise2_7A7 Exercise2_7A8 Exercise2_7A9 Exercise2_7A10 Exercise2_7A11. set (u :=Lf (fun z => Yo (evenp z) (csucc z) z) Nat Nat). set (v :=Lf (fun z => Yo (evenp z) z (csucc z)) Nat Nat). move=> ta1 ta2 c1 c2 ns. move:(Exercise2_7A6 c1) (Exercise2_7A6 c2). set (u1:= extension_to_NNstar u). set (v1:= extension_to_NNstar v). move=> c3 c4. exists NNstar, u1,v1. move: Exercise2_7A3 Exercise2_7A4 => [[oNN sNN] gNNP] iNN. have wc:forall w, closure w NNstar -> inc w (closures NNstar). move=> w wc; apply: Zo_i => //. by move: wc =>[[_ _ xx _] _ _]; apply /functionsP. move: (wc _ c3) (wc _ c4) => vc uc. split => //. move: (Exercise2_7b oNN) => [oce sce] hs. rewrite - sce // in uc vc. move: (sup_pr oce uc vc hs). set w := sup _ u1 v1. move => [/(Exercise2_7aP oNN) [_ wcl le1] /(Exercise2_7aP oNN) [_ _ le2] ale3]. have fpu: (function_prop u Nat Nat). by red; rewrite /u; aw;split => //; apply: lf_function. have fpv: (function_prop v Nat Nat). by red; rewrite /v; aw;split => //; apply: lf_function. move: (Exercise2_7A5 fpu) => /=; rewrite -/u1. move=> [upa1 upa upb [fu1 su1 tu1]]. move: (Exercise2_7A5 fpv) => /=; rewrite -/v1. move=> [vpa1 vpa vpb [fv1 sv1 tv1]]. move: (wcl) => /Zo_P [] /functionsP [fw sw tw] cw. have wp1: forall x, inc x Nat -> Q (Vf w (J x C0)) = C1. move=> x xB. have ps: (inc (J x C0) (substrate NNstar)). by rewrite sNN; apply: candu2_pra. have: (inc (Vf w (J x C0)) (substrate NNstar)). rewrite -tw; Wtac. rewrite sNN => /candu2P [p1]; case; case=> //. set (y := P (Vf w (J x C0))). move=> p2 p3. have aux: (J y C0 = Vf w (J x C0)). by symmetry;rewrite /y;apply: pair_exten;fprops; aw. have Js: (inc (J y C0) (substrate NNstar)). by rewrite sNN; apply: candu2_pra. move: (cw) => [_ _ p4]; move: (p4 _ ps);rewrite -aux => aux1. move: (le1 _ Js) (le2 _ Js) => /gNNP [p5 p6 p7] /gNNP [p8 p9 p10]. move: p7; rewrite aux1 pr2_pair; case; last first. by move => [_]; case. by move => [_ h _]; case: h. move: p10; rewrite aux1 pr2_pair; case; last first. by move => [_]; case. by move => [_ h _]; case: h. move=> [p13 _ p14] [p11 _ p12]. have aux2: Q (J y C0) = C0 by aw. move: (vpa _ Js aux2); aw; move=> [p15 _]; rewrite p15 in p14. move: (upa _ Js aux2); aw; move=> [p16 _]; rewrite p16 in p12. have yB: inc y Nat. by move: p9 => /candu2P [_]; case; case. by case: (ns _ _ yB p12 p14); aw. move: (wp1 _ NS0) NS0 => p1 ns0. set (k:= Vf w (J \0c C0)). have Js:(inc (J \0c C0) (substrate NNstar)). rewrite sNN; apply: candu2_pra; fprops. have ks: (inc k (substrate NNstar)) by rewrite /k;Wtac; rewrite sw sNN; fprops. have Pk: (inc (P k) Nat). by move: ks; rewrite sNN => /candu2P [ _ ]; case; case. move: (wp1 _ NS0) => Qk. move: cw => [[_ _ _ incf] wca wcb]. have Pk1: (forall x, gle NNstar x k -> Vf w x = k). move=> x xk. have aux : (gle NNstar (J \0c C0) x). have xs: (inc x (substrate NNstar)) by order_tac. apply/gNNP; rewrite - sNN; saw. move: xs; rewrite sNN => /candu2P [ _]; case; move => [px qx]. by constructor 1; split => //; apply: cle0n. rewrite qx;constructor 3;split;fprops. move: (incf _ _ xk)(incf _ _ aux); rewrite (wcb _ Js) -/k => r1 r2. order_tac. have q7: Vf w k = k by rewrite Pk1 //; order_tac. move: (NS_succ Pk) => SPK. set (k':= J (csucc (P k)) C1). have j's: (inc k' (substrate NNstar)). rewrite /k' sNN; apply: candu2_prb; fprops. have lt1: (glt NNstar k' k). have ha: inc k' (substrate NNstar) by rewrite /k' sNN; apply:candu2_prb. move: (cltS Pk) => [leP neP]. split. apply /gNNP; rewrite - sNN /k';saw; constructor 2. rewrite -/k Qk; split;fprops;apply: leP. by move=> kk'; move: (f_equal P kk');rewrite /k'; aw => aux;case: neP. set (ww := fun z=> Yo (gle NNstar z k') k' (Vf w z)). have ta: (lf_axiom ww (substrate NNstar) (substrate NNstar)). move=> z zs; rewrite /ww;Ytac cp => //; Wtac. set (w' := Lf ww (substrate NNstar) (substrate NNstar)). have fw': (function w') by apply: lf_function. have q3: Q k' <> C0 by rewrite /k'; aww. have q4: forall x, gle NNstar x k' -> Vf w' x = k'. by move=> x xk; rewrite /w' /ww LfV//; [ Ytac0 | order_tac]. have q5: forall x, inc x (substrate NNstar) -> ~ (gle NNstar x k') -> Vf w' x = Vf w x. by move=> x xs xk; rewrite /w' /ww LfV//; Ytac0. have q6: forall y, inc y (substrate NNstar) -> ~ gle NNstar y k' -> gle NNstar k y. move=> y ysr ng;apply /gNNP; rewrite - sNN; split => //; constructor 2. move: (ysr); rewrite sNN =>/candu2P [py]; case. move=> [pyb Qya]; case: ng;apply /gNNP; rewrite - sNN. by split => //; constructor 3. move=> [Pyb Qy]; split => //; [ rewrite Qk; fprops | rewrite Qy; fprops |]. have cy:cardinalp (P y) by fprops. have ck:cardinalp (P k) by fprops. case: (cleT_el cy ck) => //. move=> lt2; case: ng; apply /gNNP; rewrite - sNN; split => //; constructor 2. rewrite Qy;split => //; fprops. by rewrite /k'; aw; apply /cleSltP. have w1: (forall x, inc x (substrate NNstar) -> (gle NNstar (Vf u1 x) (Vf w' x) /\ gle NNstar (Vf v1 x) (Vf w' x))). move=> x xs. move: (le1 _ xs) (le2 _ xs) => le1s le2s. case: (p_or_not_p (gle NNstar x k')) => xk; last first. have ->:(Vf w' x = Vf w x) by rewrite /w' /ww LfV//; Ytac0. split => //; rewrite (q4 _ xk). rewrite (q4 _ xk). case: (equal_or_not (Q x) C0) => qx. move: (upa _ xs qx)(vpa _ xs qx) => [_ q1] [_ q2]. by split; apply /gNNP; rewrite - sNN ?q1 ?q2; split => //;try order_tac; constructor 3. by move: (upb _ xs qx)(vpb _ xs qx) => -> ->. have icw':increasing_fun w' NNstar NNstar. rewrite /w';split => //; first saw; move=> x y xy. have xs1: inc x (substrate NNstar) by order_tac. have xs2: inc y (substrate NNstar) by order_tac. case: (p_or_not_p (gle NNstar x k')) => xk; last first. have yk: ~ gle NNstar y k' by dneg wk; order_tac. by rewrite (q5 _ xs1 xk) (q5 _ xs2 yk); apply: incf. case: (p_or_not_p (gle NNstar y k')) => yk. by rewrite (q4 _ xk) (q4 _ yk); order_tac. rewrite (q4 _ xk) (q5 _ xs2 yk). move: (incf _ _ (q6 _ xs2 yk)); rewrite q7. move: lt1 => [lt1 _] le3; order_tac. have cw': (closure w' NNstar). split => //; move=> x xs. case: (p_or_not_p (gle NNstar x k')) => xk; first by rewrite (q4 _ xk). by rewrite (q5 _ xs xk); apply: wca. case: (p_or_not_p (gle NNstar x k')) => xk. rewrite (q4 _ xk); apply: q4; order_tac; order_tac. rewrite (q5 _ xs xk). case: (p_or_not_p (gle NNstar (Vf w x) k')) => xk'; last first. have ws: inc (Vf w x) (substrate NNstar) by move: (wca _ xs)=> h; order_tac. by rewrite (q5 _ ws xk'); apply: wcb. move: (incf _ _ (q6 _ xs xk)). rewrite (q4 _ xk') -/k'; rewrite q7 => aux. have aux1: gle NNstar k k' by order_tac. order_tac. have res0: inc w' (closures NNstar). by apply: Zo_i => //; apply /functionsP;split => //; rewrite /w';aw. have res1: gle (closure_ordering NNstar) u1 w'. apply /(Exercise2_7aP oNN);split => //. by apply Zo_i => //; apply /functionsP. by move=> i isr; case: (w1 _ isr). have res2: gle (closure_ordering NNstar) v1 w'. apply /(Exercise2_7aP oNN);split => //. by apply Zo_i => //; apply /functionsP. by move=> i isr; case: (w1 _ isr). move:(ale3 _ res1 res2). apply /(Exercise2_7aP oNN). move=> [_ _ bad]; move: (bad _ j's); rewrite q4; last by order_tac. move: lt1 => [lt2 lt3]. rewrite (Pk1 _ lt2) => aux; case: lt3; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)