proposition: Lemma Exercise1_15b2 (E := tripleton \0c \1c \2c) (r1 := diagonal E \cup doubleton (J \0c \2c) (J \1c \2c)) (r2 := Nint_cco \0c \2c) (f := identity E): [/\ [/\ order r1, substrate r1 = E & completion r1 = (doubleton (singleton \0c) (singleton \1c)) \cup (doubleton emptyset E)], complete_lattice r2, substrate r2 = E, increasing_fun f r1 r2 & ~(exists g, [/\ (increasing_fun g (completion_order r1) r2), (forall t, inc t E -> Vf f t = Vf g (lo_bounds r1 (singleton t)))& (forall Z, sub Z (completion r1) -> Vf g (supremum (completion_order r1) Z) = supremum r2 (Vfs g Z))])].
proof: Proof. set goal1 := [/\ _, _ & _]. set goal := [/\ _, _ , _ , _ & _]. have diag1: forall t, inc t E -> inc (J t t) (diagonal E). move => t te; apply /diagonal_pi_P; split => //. have gr1: sgraph r1. move => t; case/setU2_P; first by move => /diagonal_i_P []. case /set2_P => ->; fprops. have r1_gle: forall a b, inc (J a b) r1 -> [\/ (a = b /\ inc a E), (a = \0c /\ b = \2c) | (a = \1c /\ b = \2c)]. move => a b; case /setU2_P. by move /diagonal_pi_P => [pa pb]; constructor 1; split. case /set2_P =>h; rewrite (pr1_def h) (pr2_def h); in_TP4. have r1_refl: forall t, inc t E -> inc (J t t) r1. by move => t te; apply /setU2_P; left; apply: diag1. have sr1: substrate r1 = E. set_extens t; last by move => /r1_refl tt; substr_tac. case/(substrate_P gr1) => [] [y yi]; case: (r1_gle _ _ yi); case=> //. + by move => -> _; apply /set3_P; in_TP4. + by move => -> _; apply /set3_P; in_TP4. + by move => ->. + by move => _ ->; apply /set3_P; in_TP4. + by move =>_ -> ; apply /set3_P; in_TP4. have or1: order r1. split => //. red;rewrite sr1 //. move => y x z; rewrite /related => ta tb. case: (equal_or_not x y); [by move => -> | move => xny]. case: (equal_or_not y z); [by move => <-| move => ynz]. apply /setU2_P; right; apply /set2_P. case: (r1_gle _ _ tb) =>[] [yv hh'];first (by case: ynz); rewrite hh'. by case: (r1_gle _ _ ta) =>[] [hh yv'] => //;rewrite hh; [left | right]. case: (r1_gle _ _ ta) =>[] [hh yv'];first (by case: xny); rewrite hh;fprops. move => x y; rewrite /related => ta tb. case: (r1_gle _ _ ta); first (by move => [-> _]); move => [ta1 ta2]. case: (r1_gle _ _ tb); first (by move => [<- _]); move => [tb1 tb2]. by rewrite ta1 tb1. by rewrite ta2 tb2. case: (r1_gle _ _ tb); first (by move => [<- _]); move => [tb1 tb2]. by rewrite ta2 tb2. by rewrite ta1 tb1. move: NS2 => bs2. move: clt_12 => lt12. have le12:= proj1 lt12. have E0: inc \0c E by apply /set3_P; in_TP4. have E1: inc \1c E by apply /set3_P; in_TP4. have E2: inc \2c E by apply /set3_P; in_TP4. pose rho := up_bounds r1. pose sigma:= lo_bounds r1. set d01 := doubleton \0c \1c;set d02 := doubleton \0c \2c. set d12 := doubleton \1c \2c. set s0 := singleton \0c;set s1 := singleton \1c;set s2 := singleton \2c. have rho1: forall x, sub x E -> inc \2c (rho x). move => x xE; apply /Zo_P; rewrite sr1; split => //; split; first by ue. move => y yx;apply /setU2_P. move: (xE _ yx) =>/ set3_P; case => ->;[right | right | left ]; fprops. have rho2: rho emptyset = E. set_extens t; first by move => /Zo_P []; rewrite sr1. by rewrite - sr1; move => te; apply : Zo_i => //; split => // y /in_set0. have rho3: forall x, sub x E -> inc \2c x -> rho x = s2. move => x xE x2; apply: set1_pr; first by apply: rho1. move => z /Zo_P; rewrite sr1; move =>[ te [_ ts]]; move: (ts _ x2) => h. case: (r1_gle _ _ h) => [][] //. have rho4: rho d01 = s2. apply: set1_pr; first by apply: rho1; move => s /set2_P [] ->. move => z /Zo_P []; rewrite sr1; move => pa [_ pb]. case/set3_P:pa => tv //. move: (pb _ (set2_2 \0c \1c)) => aux. move: (r1_gle _ _ aux); rewrite tv. case=>[] [ha hb] //; by case: card1_nz. move: (pb _ (set2_1 \0c \1c)) => aux. move: (r1_gle _ _ aux); rewrite tv. by case => [] [] //; move => h _; case: card1_nz. have rho5: rho s0 = d02. rewrite /d02;set_extens t; last first. case /set2_P => ->; last by apply: rho1; apply: set1_sub. apply: Zo_i; [ue | split; [ ue | move => s /set1_P ->]]. by rewrite - sr1 in E0; order_tac. move /Zo_P => [ta [_ tb]]; move: (tb _ (set1_1 \0c)) => aux. case: (r1_gle _ _ aux);first (move => [-> _]; fprops); move => [_ ->]; fprops. have rho6: rho s1 = d12. rewrite /d12;set_extens t; last first. case /set2_P => ->; last by apply: rho1; apply: set1_sub. apply: Zo_i; [ue | split; [ ue | move => s /set1_P ->]]. by rewrite - sr1 in E1; order_tac. move => /Zo_P [ta [_ tb]]; move: (tb _ (set1_1 \1c)) => aux. case: (r1_gle _ _ aux);first (move => [-> _]; fprops);move => [_ -> ]; fprops. have sig1: forall x, sub x E -> inc \1c x -> (~ inc \0c (sigma x) /\ ~ inc \2c (sigma x)). move => x xe x1; split; move /Zo_P=> [ta [_ tb]]. case: (r1_gle _ _ (tb _ x1)); move => [h1 h2]; [by case: card1_nz |by case: (proj2 lt12) |by case: (proj2 lt12) ]. by case: (r1_gle _ _ (tb _ x1)) => [] [h1 h2]; case: (proj2 lt12). have sig2: forall x, sub x E -> inc \0c x -> (~ inc \1c (sigma x) /\ ~ inc \2c (sigma x)). move => x xe x1; split; move /Zo_P => [ta [_ tb]]. case: (r1_gle _ _ (tb _ x1)); move => [h1 h2]; first (by case: card1_nz); by case: card2_nz. by case: (r1_gle _ _ (tb _ x1))=> [] [h1 h2]; case: card2_nz. have sig0: forall x, sub (sigma x) E. by move => x t /Zo_P; rewrite sr1;case. have sig3: sigma E = emptyset. apply /set0_P=> t ts. move: (sig1 _ (@sub_refl E) E1) => [pa pb]. move: (sig2 _ (@sub_refl E) E0) => [pc _]. by move: (sig0 _ _ ts) => /set3_P [] ta; [case: pa | case: pc | case: pb ]; rewrite - ta. have sig4: sigma d12 = s1. have sdE: sub d12 E by move => t /set2_P [] ->. move: (sig1 _ sdE (set2_1 \1c \2c)) => [ta tb]. apply: set1_pr. apply: Zo_i; [ by rewrite sr1 | split; first by rewrite sr1]. move => y; case/set2_P => ->; first by apply: r1_refl. apply /setU2_P; right; fprops. move=> t ts; move: (sig0 _ _ ts)=> /set3_P [] //H; [ case: ta| case: tb]; ue. have sig5: sigma d02 = s0. have sdE: sub d02 E by move => t /set2_P [] ->. move: (sig2 _ sdE (set2_1 \0c \2c)) => [ta tb]. apply: set1_pr. apply: Zo_i; [ by rewrite sr1 | split; first by rewrite sr1]. move => y;case/set2_P => ->; first by apply: r1_refl. apply /setU2_P; right; fprops. move=> t ts; move:(sig0 _ _ ts)=> /set3_P [] //H; [ case: ta | case: tb]; ue. have sig7: sigma s0 = s0. have sdE: sub s0 E by move => t /set1_P ->. move: (sig2 _ sdE (set1_1 \0c)) => [ta tb]. apply: set1_pr. apply: Zo_i; [ by rewrite sr1 | split; first by rewrite sr1]. by move => y /set1_P ->; apply: r1_refl. move => t ts; move:(sig0 _ _ ts) => /set3_P [] //tz;[case: ta |case: tb];ue. have sig8: sigma s1 = s1. have sdE: sub (singleton \1c) E by move => t /set1_P ->. move: (sig1 _ sdE (set1_1 \1c)) => [ta tb]. apply: set1_pr. apply: Zo_i; [ by rewrite sr1 | split; first by rewrite sr1]. by move => y /set1_P ->; apply: r1_refl. move=> t ts; move:(sig0 _ _ ts)=> /set3_P [] // h; [case: ta | case: tb]; ue. have sig6: sigma s2 = E. apply: extensionality => // t tE; apply /Zo_P; rewrite/lower_bound sr1. split => //; split => // y /set1_P ->;move: tE => /set3_P;case. move => ->; apply /setU2_P; right; fprops. by move => ->; apply /setU2_P; right; fprops. by move => ->; apply: r1_refl. have cpr1: completion r1 = doubleton s0 s1 \cup doubleton emptyset E. set_extens t. move /Zo_P => [] /setP_P; rewrite sr1 /uplo_bounds. move => tE; rewrite -/rho -/sigma => ts; apply /setU2_P; move: ts. case: (p_or_not_p (inc \2c t)) => t2. move: (rho3 _ tE t2) ->; rewrite sig6 => ->; right; fprops. case: (inc_or_not \1c t) => t1; case: (inc_or_not \0c t) => t0. + suff ta: t = d01 by rewrite {2} ta rho4 sig6 => ->; right; fprops. set_extens s; last by case/set2_P => ->. move => st; case/set3_P: (tE s st) => h; rewrite h; fprops. by case: t2; ue. + suff ta: t = s1 by rewrite {2} ta rho6 sig4 => ->; left; fprops. apply: set1_pr => // s st; case/set3_P: (tE _ st) => sa //. case: t0; ue. case: t2; ue. + suff ta: t = s0 by rewrite {2} ta rho5 sig5; move ->; left; fprops. apply: set1_pr => // s st; case /set3_P: (tE _ st) => si //. case: t1; ue. case: t2; ue. + suff ta: t = emptyset by rewrite{2} ta rho2 sig3;move=> ->; right;fprops. apply /set0_P => s st;case/set3_P: (tE _ st) => si; [case: t0; ue |case: t1; ue | case: t2; ue]. move => h; apply /Zo_P; rewrite sr1 /uplo_bounds -/rho. case/setU2_P: h; case/set2_P => ->. + split; [ by apply /setP_P;apply: set1_sub | by rewrite rho5 ]. + split; [ by apply /setP_P; apply: set1_sub | by rewrite rho6 ]. + split; [ apply /setP_P;fprops | by rewrite rho2 ]. + split; [ apply /setP_P;fprops |by rewrite (rho3 _ (@sub_refl E) E2)]. have gal1T: goal1 by split. have tor2: total_order r2. move: (proj1(Ninto_wor \0c \2c)); apply: worder_total. move: (proj1 tor2) => or2. have sr2': Nintcc \0c \2c = E. set_extens t. move /(NintcP NS2)=> ts. case: (equal_or_not t \2c) => nt2; first by rewrite nt2. by case: (clt2 (conj ts nt2)) => ->. move => h; apply /(NintcP NS2). case/set3_P: h => ->;fprops; exact: (proj1 clt_02). have sr2: substrate r2 = E by rewrite (proj2(Ninto_wor \0c \2c)). have r2_gleP: forall x y, gle r2 x y <-> [/\ inc x E, inc y E & x <=c y]. move => x y; by move: (Ninto_gleP \0c \2c x y); rewrite sr2'. have cl2: complete_lattice r2. apply: Exercise1_11j => //; rewrite /ne_substrate sr2; last by ex_tac. by rewrite - sr2'; apply finite_Nintcc. have icf: increasing_fun f r1 r2. split => //. rewrite /f sr1 sr2; apply: identity_prop. move => x y le1. rewrite idV; last by rewrite - sr1; order_tac. rewrite idV; last by rewrite - sr1; order_tac. have xE: inc x E by rewrite - sr1; order_tac. have yE: inc y E by rewrite - sr1; order_tac. apply /r2_gleP; split => //; move: (r1_gle _ _ le1); case. move => [-> _]; apply: cleR; case/set3_P: yE; move => ->; fprops. move: xE; rewrite - sr2' => le2. move => [-> ->]; fprops; apply: (proj1 clt_02). move => [-> ->]; fprops. split => // [] [g [incrg cpgf cgs]]. move: (cpgf _ E0); rewrite /f (idV E0) -/sigma sig7 => g0. move: (cpgf _ E1); rewrite /f (idV E1) -/sigma sig8 => g1. move: (cpgf _ E2); rewrite /f (idV E2) -/sigma sig6 => g2. set Z := doubleton s0 s1. have Zd: sub Z (completion r1). rewrite cpr1; apply: sub_set2; apply /setU2_P; left; fprops. move: (esym (cgs _ Zd)). move: incrg => [_ _ [fg srcg trgg _]]. move: (proj2 (sub_osr (completion r1))) => hh. have zg1: sub Z (substrate (completion_order r1)) by ue. have ->: (Vfs g Z) = d01. have esg: sub Z (source g) by ue. set_extens t. move /(Vf_image_P fg esg)=> [u uz ->]; move:uz => /set2_P; case => ->; ue. case/set2_P => ->; apply /(Vf_image_P fg esg). rewrite /Z;exists s0; fprops. rewrite /Z;exists s1; fprops. have ->: supremum r2 d01 = \1c. apply: sup_comparable1 => //; apply /r2_gleP;split; fprops;apply: cle_01. suff h: supremum (completion_order r1) Z = E by rewrite h -g2;exact: card_12. move: (Exercise1_15a16 r1) => [oc h]; move: (h _ zg1) => [hs _]. move: (supremum_pr oc zg1 hs). set z := supremum _ _; move => [[za zb] zc]. move: za; rewrite hh => zr1. move /sub_gleP: (zb _ (set2_1 s0 s1)) => [_ _ ta]. move /sub_gleP: (zb _ (set2_2 s0 s1)) => [_ _ tb]. move: (ta _ (set1_1 \0c)) => z0. move: (tb _ (set1_1 \1c)) => z1. move: zr1; rewrite cpr1; case/setU2_P; case /set2_P => zt. + by move:z1; rewrite zt => /set1_P bad; case: card1_nz. + by move:z0; rewrite zt => /set1_P bad; case: card1_nz. + by move:z1; rewrite zt => /in_set0. + done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)