(** * Theory of Sets : Exercises sections 6 Copyright INRIA (2012-2013) Marelle Team (Jose Grimm). *) Require Import ssreflect ssrbool eqtype ssrfun. (* $Id: ssete6.v,v 1.90 2016/05/19 08:34:59 grimm Exp $ *) Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. Require Export sset15. Module Exercise6. Definition csup_s A := \csup (fun_image A cnext). Lemma csup_s1 A (x := csup_s A): cardinal_set A -> (forall y, inc y A -> y csa y yA. apply /(cnext_pr5P (csa _ yA)) ; apply:card_sup_ub. move => t /funI_P [z za ->]; first by exact: (CS_cnext (csa _ za)). by apply /funI_P; ex_tac. Qed. Lemma csup_s2 A z: cardinal_set A -> cardinalp z -> (forall y, inc y A -> y csup_s A <=c z. Proof. move => csa cz h2; apply: card_ub_sup => //. move => i /funI_P [t /h2 tA ->]; apply /cnext_pr5P => //; exact: (proj31_1 tA). Qed. Definition disjointness_degree F := csup_s (fun_image (coarse F -s diagonal F) (fun z => cardinal ((P z) \cap (Q z)))). Lemma dd_pr1 F x y: inc x F -> inc y F -> x <> y -> cardinal (x \cap y) xF yF xy; apply: csup_s1. move=> t /funI_P [z _ ->]; fprops. apply /funI_P; exists (J x y); aw => //. apply /setC_P;split => //; first by apply :setXp_i. by case /diagonal_pi_P. Qed. Lemma dd_pr2 F z: cardinalp z -> (forall x y, inc x F -> inc y F -> x <> y -> cardinal (x \cap y) (disjointness_degree F) <=c z. Proof. move => cz h; apply:csup_s2 => //. move=> t /funI_P [u _ ->]; fprops. move => y /funI_P [t /setC_P [/setX_P [pt Pt Qt] pb ->]]; apply: h => //. by move => xy; case: pb; apply /diagonal_i_P. Qed. Lemma dd_pr3 F : (disjointness_degree F = \0c) <-> small_set F. Proof. split => h. move => x y fx fy; ex_middle xy. by move: (dd_pr1 fx fy xy); rewrite h => /clt0. by apply: cle0; apply: (dd_pr2 CS0) => x y xf yf; move: (h _ _ xf yf). Qed. Lemma dd_pr4 F : (disjointness_degree F = \1c) <-> (~ small_set F /\ forall x y, inc x F -> inc y F -> disjointVeq x y). Proof. split => h. split; first by move /dd_pr3; rewrite h; fprops. move => x y xf yf; case: (equal_or_not x y); first by left. move => xny; move: (dd_pr1 xf yf xny); rewrite h. by move /clt1 /card_nonempty; right. move: h => [/dd_pr3 dn0 h1]; ex_middle aux. have aux2: disjointness_degree F <=c \1c. apply: (dd_pr2 CS1) => x y xF yF; case: (h1 _ _ xF yF) => // -> _. rewrite cardinal_set0 ; exact: clt_01. by case: dn0; move/clt1: (conj aux2 aux). Qed. (* ---- Exercise 6.25 *) (** -- Exercise 5.7 *) (* --------- *) Definition Noetherian r := (forall X, sub X (substrate r) -> nonempty X -> exists a, maximal (induced_order r X) a). Definition Noetherian_set r x:= sub x (substrate r) /\ Noetherian (induced_order r x). Lemma Noetherian_set_pr r x: order r -> sub x (substrate r) -> (Noetherian_set r x <-> (forall X, sub X x -> nonempty X -> exists2 a, inc a X & (forall x, inc x X -> gle r a x -> x = a))). Proof. move => or xsr; rewrite /Noetherian_set /Noetherian. rewrite (iorder_sr or xsr); split. move => [_ h] X Xx xne; move: (h _ Xx xne);rewrite (iorder_trans _ Xx). move=> [a []]; rewrite (iorder_sr or (sub_trans Xx xsr)) => ax ap. by ex_tac; move => t tX lat; apply: ap; apply /iorder_gleP. move => h; split; first by exact. move => X Xx ne; rewrite (iorder_trans _ Xx); move: (h _ Xx ne) => [a ax ap]. exists a; split; first by rewrite (iorder_sr or (sub_trans Xx xsr)). by move => b => /iorder_gle5P; move=> [_ bx ab]; apply: ap. Qed. Lemma Exercise6_29a r: order r -> Noetherian r -> Noetherian_set r (substrate r). Proof. move => or nr; split; [fprops | by rewrite (iorder_substrate or) ]. Qed. Lemma Exercise6_29b r: Noetherian_set r emptyset. Proof. split; fprops. move => X xns [w wx]; move: (xns _ wx). have ->: (induced_order r emptyset) = emptyset. by apply /set0_P => y /setI2_P [_]/setX_P [_ /in_set0]. by rewrite /substrate domain_set0 range_set0 setU2_id => /in_set0. Qed. Lemma Exercise6_29c r a b: order r -> Noetherian_set r a -> Noetherian_set r b -> Noetherian_set r (a \cup b). Proof. move => or pa pb. move: (proj1 pa) (proj1 pb) => asr bsr. move/(Noetherian_set_pr or asr):pa => pa. move /(Noetherian_set_pr or bsr):pb => pb. have usr: sub (a \cup b) (substrate r) by move=> t; case /setU2_P; [apply asr | apply: bsr]. apply/ (Noetherian_set_pr or usr). move => X Xu neX. set Xa:= X \cap a. case: (emptyset_dichot Xa) => Xane. have sb: sub X b. move => t tX; move: (Xu _ tX); case /setU2_P => // ta. empty_tac1 t; apply /setI2_P;split => //. by apply: pb. have sxa: sub Xa a by apply: subsetI2r. move: (pa _ sxa Xane) => [ea sea eap]. set Xb:= Zo X (fun t => glt r ea t). case: (emptyset_dichot Xb) => Xbne. have eax: inc ea X by move: sea;move /setI2_P=> []. exists ea => //; move => x xE le1; ex_middle ne. by empty_tac1 x; apply: Zo_i => //;split => //; apply:nesym. have sxb: sub Xb b. move => t /Zo_P [tx [le1 ne1]]. move: (Xu _ tx);case /setU2_P=> // ta. have txa: inc t Xa by rewrite /Xa; fprops. by move: (eap _ txa le1) =>eq1; case: ne1. move: (pb _ sxb Xbne) => [eb seb ebp]. have ebx: inc eb X by move: seb => /Zo_P []. exists eb => //; move => x xE le1. apply: ebp => //; apply: Zo_i => //. move: seb => /Zo_P [_ lt1]; order_tac. Qed. Lemma Exercise6_29d r X: order r -> finite_set X -> (forall x, inc x X -> Noetherian_set r x) -> Noetherian_set r (union X). Proof. move => or; move: X. apply: (finite_set_induction). move => _; rewrite setU_0; apply: Exercise6_29b. move => a n Hrec aux. have ->: union (a +s1 n) = (union a) \cup n. set_extens t. move => /setU_P [y ty] /setU1_P; case => h; apply /setU2_P; [ left;union_tac | right; ue]. case /setU2_P. move /setU_P=> [y ty ya]; union_tac. by move => tn; apply /setU_P;exists n;fprops. apply: (Exercise6_29c or); last by apply: aux; fprops. apply: Hrec=> x xa; apply: aux; fprops. Qed. Lemma Exercise6_29e r X: order r -> Noetherian r -> sub X (substrate r) -> Noetherian_set r X. Proof. move => or Nr xsr. rewrite (Noetherian_set_pr or xsr) => Y YX neY. move: (sub_trans YX xsr) => Ysr. move: (Nr _ Ysr neY) => [a []]. rewrite (iorder_sr or Ysr) => pa pb. by ex_tac; move => x xY ax; apply: pb; apply /iorder_gleP. Qed. Lemma Exercise6_29f r: order r -> (Noetherian r <-> (forall i, inc i (substrate r) -> Noetherian_set r (interval_ou r i))). Proof. move => or; split => h. by move => i isr; apply: (Exercise6_29e or h); apply: Zo_S. move => X Xsr neX. move: (neX) => [a aX]. case: (p_or_not_p (maximal (induced_order r X) a)) => ma. by exists a. set Y := Zo X (fun z => glt r a z). case: (emptyset_dichot Y) => neY. case: ma; split; first by rewrite (iorder_sr or Xsr). move => x /iorder_gle5P [_ pa pb]. by ex_middle exa; empty_tac1 x; apply: Zo_i=> //; split => //; apply: nesym. have sY: sub Y (interval_ou r a). move => y /Zo_P [yX ay]; apply /Zo_P; split => //; order_tac. fprops. move: (h _ (Xsr _ aX)). have Isr: sub (interval_ou r a) (substrate r) by apply: Zo_S. rewrite (Noetherian_set_pr or Isr) => aux. move: (aux _ sY neY) => [b ibY etc]. move: ibY => /Zo_P [bX ab]. exists b; split; first by rewrite (iorder_sr or Xsr). move=> x /iorder_gle5P [_ xX bx]. apply: etc => //;apply /Zo_P; split => //; order_tac. Qed. (* to be commented *) Definition restriction_to_segmentA r x g := [/\ order r, inc x (substrate r), function g& sub (segment r x) (source g)]. Lemma rts_function1 r x g: restriction_to_segmentA r x g -> function (restriction_to_segment r x g). Proof. move=> [p1 p2 p3 p4]. rewrite /restriction_to_segment; apply: (proj31 (restriction1_prop p3 p4)). Qed. Lemma rts_W1 r x g a: restriction_to_segmentA r x g -> glt r a x -> Vf (restriction_to_segment r x g) a = Vf g a. Proof. move=> [p1 p2 p3 p4] ax. rewrite /restriction_to_segment; apply: restriction1_V =>//. rewrite /segment/interval_uo; apply: Zo_i=>//; order_tac. Qed. Lemma rts_surjective1 r x g: restriction_to_segmentA r x g -> surjection (restriction_to_segment r x g). Proof. move=> [p1 p2 p3 p4]. rewrite /restriction_to_segment. by apply: restriction1_fs. Qed. Lemma rts_extensionality1 r s x f g: order r -> inc x (substrate r) -> order s -> inc x (substrate s) -> segment r x = segment s x -> function f -> sub (segment r x) (source f) -> function g -> sub (segment s x) (source g) -> (forall a , inc a (segment r x) -> Vf f a = Vf g a) -> restriction_to_segment r x f = restriction_to_segment s x g. Proof. move=> wor xsr wos xss srsx ff srf fg ssg sv. have rf: (restriction_to_segmentA r x f) by done. have rg: (restriction_to_segmentA s x g) by done. apply: function_exten =>//; try apply: rts_function1; try solve [rewrite /restriction_to_segment/restriction1; aw]. rewrite /restriction_to_segment/restriction1; aw. set_extens t. move/(Vf_image_P ff srf)=> [u us Wu]; apply /(Vf_image_P fg ssg). by rewrite - srsx; ex_tac; rewrite - sv. move/(Vf_image_P fg ssg)=> [u us Wu]; apply /(Vf_image_P ff srf). by rewrite - srsx in us; ex_tac; rewrite sv. move=> u;rewrite /restriction_to_segment/restriction1; aw. move=> us. have p1: glt r u x by apply: (inc_segment us). have p2: glt s u x by rewrite srsx in us;apply: (inc_segment us); ue. rewrite rts_W1 // rts_W1 // sv //. Qed. Lemma transfinite_unique11 r p f f' z: order r -> inc z (substrate r) -> transfinite_def r p f -> transfinite_def r p f' -> (forall x : Set, inc x (segment r z) -> Vf f x = Vf f' x) -> restriction_to_segment r z f = restriction_to_segment r z f'. Proof. move=> wo zsr [[ff _ ] sf Wf] [[ff' _] sf' Wf'] sW. have ss: sub (segment r z) (substrate r) by apply: sub_segment. apply: rts_extensionality1=> //; ue. Qed. Lemma inc_set_of_segments1 r x: order r -> inc x (segments r) -> segmentp r x. Proof. rewrite /segments/segmentss=> or. case /setU1_P. by move /funI_P => [z zr ->]; apply: segment_segment=>//. by move=> ->; apply: substrate_segment. Qed. (* bof Lemma transfinite_unique1 r p f f': order r -> transfinite_def r p f -> transfinite_def r p f' -> f = f'. Proof. move=> or tf tf'. set (s:=Zo(set_of_segments r) (fun z => forall x, inc x z -> Vf x f = Vf x f')). have alse:forall x, inc x s -> is_segment r x. by move => x; rewrite /Zo_P; move=>[xs _]; apply:inc_set_of_segments1. have su: forall s', sub s' s -> inc (union s') s. move=> s' s's; rewrite /s /Zo_P -inc_set_of_segments//. split. apply: union_is_segment =>//; move=> x xs'; move: (s's _ xs'); apply: alse. move=> x xu; move: (union_exists xu)=> [y [xy ys']]. by move: (s's _ ys'); rewrite /s /Zo_P; move =>[_];apply. have sc: forall x, inc x (substrate r) -> inc (segment r x) s -> inc (segment_c r x) s. move=> x xsr; rewrite /s 2! /Zo_P -inc_set_of_segments//. move=> [s1 sW]; split; first by apply: segmentc_insetof=>//. move=> y; rewrite - segment_c_pr; aw. case; first by apply: sW. *) (* ---------- *) Lemma Exercise_6_20b a: \2c (forall m, \0c m a ^c m = a) -> regular_cardinal a. Proof. move => a2 h. have ca:= proj32_1 a2. case: (finite_dichot ca). move /NatP => aB. move: (h _ clt_02 a2); rewrite cpowx2 => eq1. have aa: a <=c a by fprops. have anz: a <> \0c by move => eq2; rewrite eq2 in a2; case: (clt0 a2). move: (cprod_Mlelt aB aB aa a2 anz); rewrite eq1 => le1. case: (cltNge le1(cprod_M1le ca card2_nz)). move => ica; apply /regular_cardinalP; split; first by exact. ex_middle ne1. have sa: singular_cardinal a by split. have pa: (cpow_less_ec_prop a a \1c). split; first by apply: finite_lt_infinite; fprops. move => b; rewrite (cpowx1 ca); move /cge1P => b1 ba. by rewrite (h _ b1 ba). move: (cantor ca); rewrite - (infinite_power1_b ica). move: (cpow_less_ec_pr3 pa (proj1 a2) sa) => [-> <-]. by rewrite (cpowx1 ca); move => []. Qed. Lemma Exercise_6_20c1 a: GenContHypothesis -> regular_cardinal a -> (forall m, \0c m a ^c m = a). Proof. move => gch /regular_cardinalP [ia ra] m [_ m0] ma. move: (infinite_power10 gch m ia); move=> [_ pa _ _]. by apply: pa; [ apply:nesym | ue]. Qed. Lemma Exercise_6_20c2: (forall a, regular_cardinal a -> (forall m, \0c m a ^c m = a)) -> GenContHypothesis. Proof. move => h. move => t ict; move: (ict) => [ct _]. move: (ord_index_pr1 ict)=> [on tv]. move: (regular_initial_successor on). rewrite - (cnextE on) tv => rs. move: (h _ rs _ (finite_lt_infinite finite_0 ict) (cnext_pr2 ct)). move => le1. apply: cleA; first by apply: (cnext_pr3 ct). have pa: \2c <=c cnext t. rewrite -tv (cnextE on). apply: (finite_le_infinite finite_2 (CIS_aleph (OS_succ on))). by rewrite -le1; apply: (cpow_Mleeq _ pa card2_nz). Qed. Lemma Exercise6_22c1 x: card_dominant x -> (x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)). Proof. move => [pa pb]. move: (ord_index_pr1 pa); set c := ord_index x; move => [pd pe]. case: (ordinal_trichot pd) => ln;last by right; exists c. by left; rewrite -pe ln aleph0E. move: ln => [m om mv]. set y:= \aleph m. have yx: y le1. by move: (cnext_pr3(CS_aleph om));rewrite (cnextE om) -mv pe => /(cltNge le1). Qed. Lemma Exercise6_22c2 x (p1 := forall z, \0c z x ^c z = x) (p2:= forall z, \0c x ^c z = x *c \2c ^c z): [/\ (infinite_c x -> p1 -> p2), (card_dominant x -> (p1 <-> p2)), (card_dominant x -> p1 -> (x = omega0 \/ inaccessible x)) & (x = omega0 \/ inaccessible x -> (card_dominant x /\ p1))]. Proof. have r1:infinite_c x -> p1 -> p2. move=> icx hp1 z zp. move: (infinite_ge2 icx) => x2. move: (infinite_nz icx) => xnz. have cz:= proj32_1 zp. case: (cleT_ee (proj1 icx) (CS_pow \2c z)). move => le1. move: (ge_infinite_infinite icx le1) => icp. case: (finite_dichot cz) => icz. have f1: finite_c (\2c ^c z). by apply /NatP; apply NS_pow; fprops; rewrite inc_Nat. case: (infinite_dichot1 f1 icp). rewrite (infinite_power1 x2 le1 icz). by rewrite cprodC cprod_inf. have pnz: \2c ^c z <> \0c by apply: cpow2_nz. move => le1. rewrite (hp1 _ zp (clt_leT (cantor cz) le1)). rewrite cprod_inf //. have r2: card_dominant x -> (p1 <-> p2). move=> [icx cdx]; split; first by apply: r1. move => hp2 z z0 zx. have pnz: \2c ^c z <> \0c by apply: cpow2_nz. move: (cdx _ _ (finite_lt_infinite finite_2 icx) zx) => [l1 _]. rewrite (hp2 _ z0) cprod_inf //. have r3: card_dominant x -> p1 -> x = omega0 \/ inaccessible x. move => pa pc; case: (Exercise6_22c1 pa); first by left. move => h; right. move: pa => [pa pb]. split; last first. by move => t tx; apply: pb => //; apply: (finite_lt_infinite finite_2 pa). split; last by exact. move: (cofinality_c_small (infinite_ge2 pa)) => h1. split => //; ex_middle eq1. have pd: \0c [_]. split => //. case => ix. rewrite ix; split; first by apply: card_dominant_pr2. move => z z0 zf. have pa: infinite_c x by rewrite ix; apply: CIS_omega. have pb: inc z Nat. by rewrite ix in zf; move: (oclt zf) => /oltP0 [_ _]. have pc: z <> \0c by move: z0 => [_ /nesym]. by rewrite cpow_inf. split; first by apply: inaccessible_dominant. by move => z [_ zc] zx;apply: inaccessible_pr7 => //; apply:nesym. Qed. (************************************************* *) (** Exercise 6 33 *) Lemma CIS_next x: infinite_c x -> infinite_c (cnext x). Proof. move => icx. move: (cnext_pr1 (proj1 icx)) => [_ [ha _] _]. exact: (ge_infinite_infinite icx ha). Qed. Section Exercise6_33. Variables a b E F: Set. Hypothesis ha: \2c <=c a. Hypothesis hb: \1c <=c b. Hypothesis iab: infinite_c a \/ infinite_c b. Hypothesis HF0: sub F (powerset E). Hypothesis HF1: a ^c b cardinal x <=c b. Definition Ex6_33_conc:= exists G q, [/\ sub G F , a ^c b inc b G -> a <> b -> intersection2 a b = q]. Lemma Exercise6_33a: infinite_c (a ^c b). Proof. have bnz := nesym (proj2(clt_leT clt_01 hb)). case iab => iiab; [apply: (CIS_pow iiab bnz) | apply:(CIS_pow3 ha iiab) ]. Qed. Lemma Exercise6_33a': a ^c (b *c b) = a ^c b. Proof. case: (finite_dichot (proj32 hb)) => fb; last by rewrite csquare_inf. case: iab => fa; last by rewrite csquare_inf. move: fb => /NatP fb. by rewrite cpow_pow {1} (cpow_inf fa fb (nesym (proj2(clt_leT clt_01 hb)))). Qed. Definition E6_33_c := cnext (a ^c b). Lemma Exercise6_33c: infinite_c E6_33_c. Proof. exact: (CIS_next Exercise6_33a). Qed. Lemma Exercise6_33b : a ^c b injection_prop f E6_33_c (F -s1 emptyset)). Definition E6_33_M := unionb (Lg E6_33_c (Vf E6_33_X)). Lemma Exercise6_33d (f := E6_33_X): injection_prop f E6_33_c (F -s1 emptyset). Proof. suff:exists f0, injection_prop f0 E6_33_c (F -s1 emptyset) by apply:choose_pr. apply/eq_subset_ex_injP/eq_subset_cardP1. move:(ge_infinite_infinite Exercise6_33a (proj1 HF1)) => /infinite_setP iF. rewrite - (card_setC1_inf _ iF) (card_card (proj1 Exercise6_33c)). by apply/(cnext_pr5P (proj31_1 HF1)). Qed. Lemma Exercise6_33d' n: inc n E6_33_c -> inc (Vf E6_33_X n) F. Proof. move: Exercise6_33d => [[fx ix] <- tx] ns. by move: (Vf_target fx ns); rewrite tx => /setC1_P []. Qed. Lemma Exercise6_33d'' n: inc n E6_33_c -> nonempty (Vf E6_33_X n). Proof. move: Exercise6_33d => [[fx ix] <- tx] ns. by move: (Vf_target fx ns); rewrite tx => /setC1_P [_] /nonemptyP. Qed. Lemma Exercise6_33e n: inc n E6_33_c -> sub (Vf E6_33_X n) E6_33_M. Proof. move: Exercise6_33d => [[fx ix] sx tx]. rewrite /E6_33_M => nc t tw; apply /setUb_P; bw;ex_tac; bw. Qed. Lemma Exercise6_33f: cardinal E6_33_M = E6_33_c. Proof. have bnz := nesym (proj2(clt_leT clt_01 hb)). have le: cardinal E6_33_M <=c E6_33_c. set f := (Lg E6_33_c (fun z => Vf E6_33_X z)). apply: (cleT (csum_pr1 f)). set f1 := (Lg (domain f) (fun z => cardinal (Vg f z))). set g := cst_graph E6_33_c b. have f1x: fgraph f1 by rewrite /f1/cst_graph; fprops. have gx: fgraph g by rewrite /g/cst_graph; fprops. have sd: domain f1 = domain g by rewrite /f1 /g /f /cst_graph; bw. have le1: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg g x). rewrite /f1/f/g/cst_graph; bw => x xd; bw. by apply: HF2; apply:Exercise6_33d'. move: (csum_increasing sd le1); rewrite /g csum_of_same. by rewrite cprodC (cprod_inf (proj2 Exercise6_33a'') Exercise6_33c bnz). move: (le) => [_ cc _]. set T1:= fun_image (functions b E6_33_M) Imf; set T := T1 +s1 emptyset. move: (Exercise6_33d) => [[fx ix] sx tx]. have pa: forall i, inc i E6_33_c -> inc (Vf E6_33_X i) T. move => i ic. move: (ic); rewrite - sx => ic'. move: ((Vf_target fx) _ ic'); rewrite tx =>/setC1_P [wf _]. move: (HF2 wf) => cl. case: (emptyset_dichot (Vf E6_33_X i))=> wne; first by rewrite wne /T; fprops. apply /setU1_P; left; aw. move: cl; rewrite - {1} (card_card (proj32 hb)) => le2. have [c cb ecb]: equipotent_to_subset (Vf E6_33_X i) b. apply /(eq_subset_cardP); exact: (cardinal_le_aux1 le2). have [f [bf sf tf]]: c \Eq Vf E6_33_X i by apply: EqS. pose g z := Yo (inc z c) (Vf f z) (rep (Vf E6_33_X i)). have pa: forall z, inc (g z) (Vf E6_33_X i). move => z; rewrite /g; Ytac zc; last by apply: rep_i. rewrite -tf; Wtac; fct_tac. have pb: forall z, inc z (Vf E6_33_X i) -> exists2 i, inc i b & g i = z. rewrite -tf; move=> z ztf; move: ((proj2 (proj2 bf)) _ ztf)=> [y ysf <-]. rewrite sf in ysf; exists y; [by apply: cb | by rewrite /g; Ytac0]. have pc: lf_axiom g b E6_33_M. move => z zb; move: (pa z) => i1; apply /setUb_P; bw; ex_tac; bw. set G := Lf g b E6_33_M. have fg: function G by apply: lf_function. have pd: inc G (functions b E6_33_M). by rewrite /G;apply /functionsP;split => //; aw. apply /funI_P;ex_tac; symmetry;set_extens t. move /(Vf_image_P1 fg) => [u usg ->]. rewrite /G; aw; move: usg; rewrite /G;aw. move => tw; move: (pb _ tw) => [z zi <-]; apply /(Vf_image_P1 fg). exists z; rewrite /G; aw;split => //. have : equipotent_to_subset E6_33_c T. rewrite eq_subset_ex_injP. exists (Lf (fun z => (Vf E6_33_X z)) E6_33_c T); split; aw. apply: lf_injective; first by apply: pa. rewrite - sx; apply: ix. move /eq_subset_cardP1; rewrite (card_card cc) => eq1. set aa:= (functions b E6_33_M). have sj: (surjection (Lf Imf aa (fun_image aa Imf))). apply: lf_surjective. by move=> t ta; apply /funI_P;exists t. by move=> y /funI_P. move: (image_smaller (proj1 sj)). move: (surjective_pr0 sj); aw; move => ->; rewrite /aa -/T1. rewrite cpow_pr1 (card_card (proj32 hb)). have -> : cardinal T1 = cardinal T. case: (inc_or_not emptyset T1) => eT. by rewrite /T (setU1_eq eT). move: Exercise6_33c => i1. move: (ge_infinite_infinite Exercise6_33c eq1) => /infinite_setP it. by rewrite (card_setC1_inf emptyset it) /T (setU1_K eT). move => l2; move: (cleT eq1 l2) => l3. case: (equal_or_not (cardinal E6_33_M) \0c) => mz. by move:l3; rewrite mz (cpow0x bnz) => h; symmetry; apply: cle0. ex_middle ne. have le1:=(cnext_pr4 (proj31_1 HF1) (conj le ne)). move: (cpow_Mleeq b le1 mz); rewrite - cpow_pow Exercise6_33a' => l1. case: (cltNge Exercise6_33b (cleT l3 l1)). Qed. Definition E6_33_x:= equipotent_ex E6_33_c E6_33_M. Definition E6_33_r := Vfs (ext_to_prod E6_33_x E6_33_x) (ordinal_o E6_33_c). Definition E6_33_rho n := ordinal (induced_order E6_33_r (Vf E6_33_X n)). Lemma Exercise6_33g : bijection_prop E6_33_x E6_33_c E6_33_M. Proof. apply:equipotent_ex_pr; apply/card_eqP. by rewrite Exercise6_33f (card_card (proj1 Exercise6_33c)). Qed. Lemma Exercise6_33h (x := E6_33_x) (r:= E6_33_r) (c := E6_33_c): [/\ worder_on r E6_33_M, order_isomorphism x (ordinal_o E6_33_c) r & (forall a b, inc a c -> inc b c -> (a <=o b <-> gle r (Vf x a) (Vf x b)))]. Proof. have oc:= (proj1 (proj1 Exercise6_33c)). move: (ordinal_o_wor oc) => wo1; move: (wo1) => [o1 _]. have sr1:= (ordinal_o_sr E6_33_c). move: Exercise6_33g; rewrite -/x; move => [bx sx tx]. rewrite -{2} sx in sr1. move: (order_transportation bx o1 sr1); rewrite /x -/ E6_33_r -/r => oi1. move: (oi1) => [_ or [_ _ sr2] xinc]. hnf in xinc; rewrite tx in sr2; rewrite sx in xinc. have wo: worder r by apply: worder_invariance wo1; exists E6_33_x. split => //. move => u v ux vx; rewrite - (xinc _ _ ux vx); split. move => [_ _ h]; apply /ordo_leP;split => //. by move /ordo_leP => [_ _ h]; split => //; apply: (ordinal_hi oc). Qed. Lemma Exercise6_33i n: inc n E6_33_c -> [/\ worder (induced_order E6_33_r (Vf E6_33_X n)), ordinalp (E6_33_rho n), E6_33_rho n <> \0o & cardinal(E6_33_rho n) <=c b]. Proof. move => ni; rewrite /E6_33_rho. set r := induced_order _ _. move: Exercise6_33h => [[wo1 sr] oi oie]. move: (Exercise6_33e ni); rewrite - sr => pa. have wor: worder r by move: (induced_wor wo1 pa). move: Exercise6_33d => [[fx ix] ss tx]; rewrite - ss in ni. move: (Vf_target fx ni); rewrite tx => /setC1_P [/HF2 hc hd]. have he: ordinal r <> \0o. move => h2; move:(ordinal0_pr2 wor h2); rewrite /r iorder_sr;fprops. split; [ exact | by apply: OS_ordinal | exact | ]. by rewrite (cardinal_of_ordinal wor) (iorder_sr (proj1 wo1) pa). Qed. Definition E6_33_y n := the_ordinal_iso (induced_order E6_33_r (Vf E6_33_X n)). Definition E6_33_Mi m := Zo E6_33_M (fun z => exists n, [/\ inc n E6_33_c, inc m (source (E6_33_y n)) & z = Vf (E6_33_y n) m]). Definition E6_33_al := intersection (Zo (a ^c b) (fun m => (cardinal (E6_33_Mi m) = E6_33_c))). Lemma Exercise6_33j n (yn := E6_33_y n) (r := induced_order E6_33_r (Vf E6_33_X n)): inc n E6_33_c -> [/\ order_isomorphism yn (ordinal_o (E6_33_rho n)) r, source yn = E6_33_rho n & target yn = (Vf E6_33_X n)]. Proof. move=> nc. have pa: order_isomorphism yn (ordinal_o (E6_33_rho n)) r. by apply: the_ordinal_iso1; move: (Exercise6_33i nc) => []. move: (pa) => [_ _ [_ -> ->] _]. move: (Exercise6_33h) => [[pe pf] _ _]. by rewrite ordinal_o_sr /r (iorder_sr (proj1 pe)) // pf;apply: Exercise6_33e. Qed. Lemma Exercise6_33k n: inc n E6_33_c -> ((forall t, inc t (E6_33_rho n) -> t ns. have [_ qa _ qb] := (Exercise6_33i ns). move/(ocle2P (CS_pow a b) qa): (cle_ltT qb (proj1 (Exercise6_33a''))) => h. split. move => t /(oltP qa) [pa _]; exact: (ole_ltT pa h). have o3: ordinalp E6_33_c by exact (proj1 (proj1 Exercise6_33c)). move: h Exercise6_33b => [[_ _ s1] _] [[_ _ s2] _]. apply: (sub_trans s1 s2). Qed. Lemma Exercise6_33l: E6_33_M = unionf (a ^c b) E6_33_Mi. Proof. set_extens x; last by move /setUf_P => [y yp /Zo_S]. move: Exercise6_33d => [[fc ix] sx tx]. move => xM; move: (xM) => /setUb_P; bw; move => [y ys]; bw => xW. move: (Exercise6_33j ys) => [[o1 o2 [bf sf tf] _] sy ty]. rewrite - ty in xW. move: (proj2 (proj2 bf) _ xW) => [n ns xv]. move: (proj1 (Exercise6_33k ys)); rewrite - sy => s1. move: (olt_i (s1 _ ns)) => np. by apply /setUf_P; exists n => //; apply: (Zo_i xM); exists y. Qed. Lemma Exercise6_33m x (c:= cardinal (E6_33_Mi x)): inc x (a ^c b) -> c <=c (a ^c b) \/ c = E6_33_c. Proof. move: Exercise6_33l => eq1 xs. have s1: sub (E6_33_Mi x) E6_33_M. move =>t ti; rewrite eq1; apply /setUf_P; ex_tac. move: (sub_smaller s1); rewrite Exercise6_33f => le1. case: (equal_or_not c E6_33_c) => cc; [by right | left]. by apply: (cnext_pr4 (proj31_1 HF1)). Qed. Lemma csum_pr1_bnd X f c: (forall i, inc i X -> cardinal (f i) <=c c) -> cardinal (unionf X f) <=c c *c X. Proof. move => H. move: (csum_pr1 (Lg X f)). have ->: unionb (Lg X f) = unionf X f. rewrite /unionb; bw;apply:setUf_exten => x xs;bw. rewrite /csumb Lg_domain - csum_of_same. set f1 := Lg _ _ => l1. set f2 := cst_graph X c. have sd: domain f1 = domain f2 by rewrite /f1/f2/cst_graph; bw. have pb: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg f2 x). by rewrite /f1/f2/cst_graph;bw => x xa; bw; apply:H. exact: (cleT l1 (csum_increasing sd pb)). Qed. Lemma Exercise6_33n: exists2 m, m x xab; case: (Exercise6_33m xab) => // e1. by case: pa; exists x => //; apply/(oltP (proj1 (proj31_1 HF1))). Qed. Lemma Exercise6_33o (al:= E6_33_al): [/\ al cardinal (E6_33_Mi m) <=c (a ^c b))]. Proof. rewrite /al /E6_33_al; set Z := Zo _ _. have oab: ordinalp (a ^c b) by move: (CS_pow a b) => []. have nez: nonempty Z. move: Exercise6_33n => [m /olt_i ml]; exists m; apply: Zo_i=> //. have oz: ordinal_set Z by move=> t => /Zo_P [/(ordinal_hi oab) tab _]. move: (least_ordinal0 oz nez) => [_ /Zo_P [/(oltP oab) lt pb] hz]. split => // m mc; move: (olt_leT mc (proj1 lt)) =>/(oltP oab) mab. by case:(Exercise6_33m mab)=> // eq1; case: (oltNge mc); apply: hz; apply: Zo_i. Qed. Lemma Exercise6_33p: cardinal (unionf E6_33_al E6_33_Mi) <=c a ^c b. Proof. have [h1 h2 h3]:=Exercise6_33o;have h0:= (proj31_1 h1). move/(ocle2P (proj31_1 HF1) h0): h1 => h5. move: (cprod_inf1 (proj1 h5) Exercise6_33a); rewrite cprod2cr. by apply: cleT; apply:csum_pr1_bnd => m mi;apply: h3; move/(oltP h0): mi. Qed. Definition E6_33_N0 := fun_image (E6_33_Mi E6_33_al) (fun t => rep (Zo E6_33_c (fun n => inc E6_33_al (source (E6_33_y n)) /\ Vf (E6_33_y n) E6_33_al = t))). Lemma Exercise6_33q (N0 := E6_33_N0) (al := E6_33_al) (Ma := E6_33_Mi E6_33_al): [/\ forall t, inc t N0 -> [/\ inc t E6_33_c, inc al (source (E6_33_y t))& inc (Vf (E6_33_y t) al) Ma], (forall t1 t2, inc t1 N0 -> inc t2 N0 -> (Vf (E6_33_y t1) al) = (Vf (E6_33_y t2) al) -> t1 = t2), (forall s, inc s Ma -> exists2 t, inc t N0 & s = (Vf (E6_33_y t) al)), sub N0 E6_33_c & cardinal N0 = E6_33_c]. Proof. pose Z z := Zo E6_33_c (fun n => inc E6_33_al (source (E6_33_y n)) /\ Vf (E6_33_y n) E6_33_al = z). have znz: forall z, inc z (E6_33_Mi E6_33_al) -> nonempty (Z z). by move => z /Zo_P [zM [n [nc als zv]]]; exists n; apply: Zo_i. have pa: forall t, inc t N0 -> [/\ inc t E6_33_c, inc al (source (E6_33_y t)) & inc (Vf (E6_33_y t) al) Ma]. move => t /funI_P [z z1 rz]. move: (rep_i (znz _ z1)); rewrite rz; move /Zo_P => [pa [pb pc]]. split => //; rewrite pc //. have pb: (forall t1 t2, inc t1 N0 -> inc t2 N0 -> (Vf (E6_33_y t1) al) = (Vf (E6_33_y t2) al) -> t1 = t2). move => t1 t2 t1n t2n sv. move: t1n => /funI_P [z z1 rz]. move: (rep_i (znz _ z1)); rewrite rz; move => /Zo_hi [_ pc]. move: t2n => /funI_P [z' z1' rz']. move: (rep_i (znz _ z1')); rewrite rz'; move /Zo_hi => [_ pc']. by move: pc pc' sv; rewrite - {1}rz - {1} rz' -/al => -> -> ->. have pc: (forall s, inc s Ma -> exists2 t, inc t N0 & s = Vf (E6_33_y t) al). move => s sm. set u := rep (Z s). have un: inc u N0 by apply /funI_P; rewrite -/Ma; exists s => //. exists u => //. by move: (rep_i (znz _ sm)) => /Zo_P [_ [_ ->]]. split => //. move => t tn; exact: (proj31 (pa _ tn)). set f:= Lf (fun t => Vf (E6_33_y t) al) N0 Ma. have bf: bijection f. by apply: lf_bijective => // t ta; move: (pa _ ta) => [_ _ ok]. have: (source f \Eq target f) by exists f; split => //. rewrite /f; aw; move /card_eqP. by rewrite - (proj32 Exercise6_33o). Qed. Variable Nf: Set-> Set. Variable zf: Set -> Set. Hypothesis NFhyp1: forall b, b sub (Nf b) E6_33_N0. Hypothesis NFhyp2: forall b, b forall n c, c <=o b -> inc n (Nf b) -> Vf (E6_33_y n) c = zf c. Hypothesis NFhyp3: forall b, b cardinal (Nf b) = E6_33_c. Lemma Exercise6_3r: cardinal (intersectionf E6_33_al Nf) = E6_33_c. Proof. apply:cleA. have: sub (intersectionf E6_33_al Nf) (Nf \0c). move => t ti; apply:(setIf_hi ti). admit. admit. admit. Qed. End Exercise6_33. End Exercise6. (** ** The von Neuman ordinals *) Module VonNeumann. (** A [numeration] is a functional graph [f] such that [f(x)] is the set of all [f(y)] where [y Vg f x = direct_image f (segment r x)]. Definition numerable r := worder r /\ exists f, numeration r f. (** Each set has at most one numeration *) Lemma direct_image_exten f f' a: fgraph f -> fgraph f' -> (forall x, inc x a -> Vg f x = Vg f' x) -> sub a (domain f) -> sub a (domain f') -> direct_image f a = direct_image f' a. Proof. move=> fgf fgf' sVVg adf adf'. set_extens x; move /dirim_P => [u us Jg]; apply /dirim_P; ex_tac. move: (pr2_V fgf Jg); aw; move=> ->; rewrite (sVVg _ us). by apply: fdomain_pr1 =>//; apply: adf'. move: (pr2_V fgf' Jg); aw; move=> ->; rewrite -(sVVg _ us). by apply: fdomain_pr1 =>//; apply: adf. Qed. Lemma numeration_unique r f f': worder r -> numeration r f -> numeration r f' -> f = f'. Proof. move=> [or wor] [fgf df Vf][fgf' df' Vf']. set A :=Zo (substrate r)(fun x=> Vg f x <> Vg f' x). case: (emptyset_dichot A)=> neA. apply: (fgraph_exten fgf fgf'); rewrite df => // a xdf. by ex_middle nVV; empty_tac1 a; apply: Zo_i. have sAs: sub A (substrate r) by apply: Zo_S. move: (wor _ sAs neA)=> [y []]; aw => yA leyA. move: (sAs _ yA)=> ysr. have srp: forall z, inc z (segment r y) -> Vg f z = Vg f' z. move=> z /segmentP zy; ex_middle nVV. have zA: (inc z A) by apply: Zo_i=>//; order_tac. move: (iorder_gle1 (leyA _ zA)) => yz; order_tac. have nyA: Vg f y = Vg f' y. rewrite df in Vf; rewrite df' in Vf'. rewrite Vf // Vf' //. apply: direct_image_exten =>//. rewrite df; apply: sub_segment. rewrite df'; apply: sub_segment. by move: yA => /Zo_P [_ []]. Qed. (** A numeration of a segment is obtained by restriction *) Lemma sub_numeration r f x: let r' := induced_order r (segment r x) in worder r -> numeration r f -> inc x (substrate r) -> numeration r' (restr f (segment r x)). Proof. move=> r' wor num xsr. have sss:= (@sub_segment r x). have wor':=(induced_wor wor sss). have [fgf df pf]:= num. have sr':substrate r' = (segment r x) by rewrite /r'; aw; fprops. have ssd: sub (segment r x) (domain f) by ue. have dr:domain (restr f (segment r x)) = substrate r' by bw. split;bw;fprops => a asr. have sra: (segment r' a = segment r a). apply: segment_induced_a =>//; fprops. apply: segment_segment; fprops. rewrite sra (restr_ev _ asr) pf; last by apply:ssd. have ssad: sub (segment r a) (domain f) by rewrite df; apply:sub_segment. have sax: sub (segment r a) (segment r x). move=> t; move: asr => /segmentP p1 /segmentP p2. have or: order r by fprops. apply /segmentP;order_tac. apply: direct_image_exten; bw; fprops. by move=> z zs; rewrite restr_ev => //; apply: sax. Qed. (** If all segments are numerable so is the whole set *) Lemma segments_numerables r: let r' := fun x => induced_order r (segment r x) in worder r -> (forall x, inc x (substrate r)-> numerable (r' x)) -> numerable r. Proof. move=> r' wor aln. set f:= (fun x => choose (fun y=> numeration (r' x) y)). have fp: forall x, inc x (substrate r) -> numeration (r' x) (f x). by move=> x xsr; move: (aln _ xsr)=> [_ c];rewrite /f;apply: choose_pr. have or: order r by fprops. have restrp: forall x y, glt r y x -> f y = restr (f x) (substrate (r' y)). move=> x y ryx. have sss: sub (segment r x) (substrate r) by apply: sub_segment. have ssy: sub (segment r y) (substrate r) by apply: sub_segment. have p6: worder (r' y) by apply: induced_wor =>//. apply: (numeration_unique p6); first by apply: fp; order_tac. have <-: (segment (r' x) y) = substrate (r' y). rewrite /r'; aw; try apply: sub_segment; rewrite segment_induced //. have p1: worder (r' x) by rewrite /r'; apply: induced_wor =>//. have p2: numeration (r' x) (f x) by apply: fp; order_tac. have p3: inc y (substrate (r' x)) by rewrite /r'; aw; apply /segmentP. move: (sub_numeration p1 p2 p3). have -> //: induced_order (r' x) (segment (r' x) y) = r' y. rewrite /r' segment_induced // iorder_trans //. apply: (segment_monotone or (proj1 ryx)). have gp: forall x y, glt r y x -> range (f y) = Vg (f x) y. move=> x y yx. have xsr: (inc x (substrate r)) by order_tac. have ysr: (inc y (substrate r)) by order_tac. move: (fp _ xsr) => [fg df vf]. move: df; rewrite /r' ; aw => df; last by apply: sub_segment. have ysrx: (inc y (segment r x)) by apply /segmentP. rewrite df in vf; rewrite (vf _ ysrx) (restrp _ _ yx). have ->: (segment (r' x) y) = (substrate (r' y)). rewrite /r'; aw; [ by rewrite segment_induced | apply: sub_segment]. have gr: sgraph (restr (f x) (substrate (r' y))) by fprops. have fgr: fgraph (restr (f x) (substrate (r' y))) by fprops. have hh: sub (substrate (r' y)) (domain (f x)). rewrite df; rewrite /r' (iorder_sr or (@sub_segment r y)). apply:(segment_monotone or (proj1 yx)). set_extens u. move /(range_gP fgr); bw; move => [z pa pb]; apply /dirim_P; exists z => //. by move: pb; bw => ->; apply:(fdomain_pr1 fg); apply: hh. move /dirim_P => [z za zb];apply /(range_gP fgr); exists z; bw. move: (pr2_V fg zb); aw. split =>//; exists (Lg (substrate r) (range \o f)). red; bw; split;fprops. move=> x xsr; bw. move: (fp _ xsr) => [ff df vf]. move: df; rewrite /r' ; aw => df; last by apply: sub_segment. have gf: sgraph (f x) by fprops. have p0: sub (segment r x) (substrate r) by apply: sub_segment. have fgL: fgraph (Lg (substrate r) (range \o f)) by fprops. set_extens t. move=> /(range_gP ff) [z pa pb]; apply /dirim_P; exists z; first ue. move: pa; rewrite df => /segmentP h; rewrite pb - (gp _ _ h); apply: Lg_i. order_tac. move /dirim_P => [z xs JL]; move: (p0 _ xs) => zs. move /segmentP: (xs) => lt1. move: (pr2_V fgL JL); aw; bw => -> /=; rewrite (gp _ _ lt1). by apply /(range_gP ff); exists z => //; ue. Qed. (** Any well-ordered is numerable *) Lemma worder_numerable r: worder r -> numerable r. Proof. move=> wor; apply: segments_numerables =>// x xsr. set r' := fun x => induced_order r (segment r x). set (A:= Zo (substrate r)(fun z=> ~numerable (r' z))). case: (p_or_not_p (numerable (induced_order r (segment r x)))) =>// h. have sA: (sub A (substrate r)) by apply: Zo_S. have neA: nonempty A by exists x; apply/Zo_P. move: (wor)=> [or aux]; move: (aux _ sA neA)=> [y []]; aw=> ys yp. have rec: forall z, glt r z y -> numerable (r' z). move=>z zy; case: (p_or_not_p (numerable (r' z))) =>// nnz. have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac. move: (iorder_gle1 (yp _ zA)) => yz; order_tac. move: ys => /Zo_P [ys ny]; case: ny. have sss: sub (segment r y) (substrate r) by apply: sub_segment. apply: segments_numerables; first by apply: induced_wor. rewrite /r'; aw; move=> z zy. have rzy: glt r z y by apply /segmentP. rewrite segment_induced // iorder_trans //;first by apply: rec. apply: segment_monotone =>//; order_tac. Qed. (** The previous result is obvious by [transfinite_defined] *) Lemma worder_numerable_bis r: worder r -> numeration r (graph (ordinal_iso r)). Proof. move=> wor. move: (transfinite_defined_pr target wor) => [suf sf vf]. have ff:= proj1 suf. hnf; rewrite (f_domain_graph ff) sf; split; fprops. move=> x xsr; move: (vf _ xsr); rewrite /Vf; move=> ->; apply:corresp_t. Qed. End VonNeumann. (** ---- *) Module OrderType. (** ** Bourbaki Exercices Order Types*) (* not used *) Lemma oprod0r' x: ordinalp x -> x *o \0o = \0o. Proof. by move => ox; rewrite (oprod_rec_def ox OS0) setX_0r funI_set0. Qed. Lemma oprod0l' x: ordinalp x -> \0o *o x = \0o. Proof. by move => ox; rewrite (oprod_rec_def OS0 ox) setX_0l funI_set0. Qed. Lemma osum_assoc2 a b c: order a -> order b -> order c -> (order_sum2 a (order_sum2 b c)) \Is (order_sum2 (order_sum2 a b) c). Proof. move=> oa ob oc. have oab: order (order_sum2 a b) by fprops. have obc: order (order_sum2 b c) by fprops. set E:= substrate (order_sum2 a (order_sum2 b c)). set F:= substrate (order_sum2 (order_sum2 a b) c). set A:= substrate a; set B := substrate b; set C := substrate c. have Ev: E = canonical_du2 A (canonical_du2 B C). by rewrite /E ! orsum2_sr. have Fv: F = canonical_du2 (canonical_du2 A B) C. by rewrite /F ! orsum2_sr. move: C1_ne_C0 => nT. move: C0_ne_C1 => nT1. set f := fun z => Yo (Q z = C0) (J (J (P z) C0) C0) (Yo (Q (P z) = C0) (J (J (P (P z)) C1) C0) (J (P (P z)) C1)). have p1: forall x, inc x E -> inc (f x) F. move => x; rewrite Ev Fv; move /candu2P => [px]; case. by move=> [PA Qa]; rewrite /f; Ytac0; apply: candu2_pra; apply: candu2_pra. move => [] /candu2P [pPx alt] Qb. have nQa: Q x <> C0 by rewrite Qb. rewrite /f; Ytac0. case: alt;move => [Ppx Qpx]. by Ytac0; apply: candu2_pra; apply: candu2_prb. rewrite (Y_false); [ apply: candu2_prb => // | rewrite Qpx; fprops]. have p2: forall y, inc y F -> exists2 x, inc x E & y = f x. move => y; rewrite Ev Fv; move /candu2P => [px]; case. move=> [] /candu2P [pPy aux] Qpy; case: aux. move=> [PPa QP]; exists (J (P (P y)) C0). by apply: candu2_pra. rewrite /f pr2_pair; Ytac0; aw. apply: pair_exten =>//; fprops; aw; try ue. move=> [PPy QPy]; exists (J (J (P (P y)) C0) C1). by apply: candu2_prb; apply: candu2_pra. rewrite /f !(pr1_pair, pr2_pair); Ytac0; Ytac0. apply: pair_exten =>//; fprops; aw; try ue. move=> [Py Qy]; exists (J (J (P y) C1) C1). by apply: candu2_prb; apply: candu2_prb. rewrite /f !(pr2_pair, pr1_pair); Ytac0; Ytac0. apply: pair_exten =>//;fprops; aw;ue. have p3: forall x y, inc x E -> inc y E -> f x = f y -> x = y. move => x y; rewrite Ev; move /candu2P => [px hx] /candu2P [py hy]. rewrite /f;case: hx. move => [PxA Qxa]; Ytac0. case: hy. move => [PyA Qya]; Ytac0 => sf; move:(pr1_def sf). by rewrite - {1} Qxa - Qya px py. move=> [_ ] Qy; rewrite Qy; Ytac0; Ytac h1. move => h2;case: nT1; exact: (pr2_def(pr1_def h2)). move => h2;case: nT1; exact: (pr2_def h2). move => [] /candu2P [pPx auxx] Qx; rewrite Qx; Ytac0. case: hy. move=> [_ Qy]; Ytac0; Ytac h. move => h2;case: nT; exact: (pr2_def(pr1_def h2)). move => h2;case: nT; exact: (pr2_def h2). move=> [] /candu2P [pPy auxy] Qy; rewrite Qy; Ytac0. case: auxx; move=> [PPx Qpx]. Ytac0. case: auxy; move=> [PPy Qpy]. Ytac0 => sf; move: (pr1_def (pr1_def sf)) => sf1. apply: pair_exten =>//; try ue. apply: pair_exten =>//; try ue. rewrite Qpy;Ytac0=> sf; case: nT1; exact: (pr2_def sf). case: auxy; move=> [_ Qpy]. rewrite Qpx Qpy; Ytac0; Ytac0 => sf; case: nT; exact: (pr2_def sf). rewrite Qpx Qpy; Ytac0; Ytac0. move=> sf; move: (pr1_def sf) => sf1. apply: pair_exten =>//; try ue. apply: pair_exten =>//; try ue. exists (Lf f E F); split;fprops;aw. split; aw;apply: lf_bijective => //. red; rewrite lf_source;move=> x y xE yE; aw. move: (xE); rewrite Ev ; move=> /candu2P [px hx]. move: (yE); rewrite Ev ; move=> /candu2P [py hy]. split. move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP; rewrite orsum2_sr //. split => //; first by move: (p1 _ xE); rewrite Fv. by move: (p1 _ yE); rewrite Fv. case: h. move=> [Qx Qy le]; constructor 1; rewrite /f (Y_true Qx) (Y_true Qy). rewrite ! pr1_pair ! pr2_pair; split => //. apply /orsum2_gleP;split => //; last by aw; constructor 1. apply candu2_pra; order_tac. apply candu2_pra; order_tac. move => [hxa hxb] /orsum2_gleP [_ _]. case: hx; move => [pxa qxa]; first by case: hxa. case: hy; move => [pya qya]; first by case: hxb. case; last first. by move => [sa sb]; constructor 3; rewrite /f; do 4 Ytac0; aw. by move => [sa sb sc];constructor 2; rewrite /f; do 4 Ytac0; aw. move => [sa sb sc]; constructor 1; rewrite /f; do 4 Ytac0; aw. case /candu2P: pxa => _ [] [ta tb]; last by case: nT; rewrite - sa - tb. case /candu2P: pya => _ [] [ta' tb']; last by case: nT; rewrite - sb - tb'. split => //; apply/orsum2_gleP; split => //. by apply: candu2_prb. by apply: candu2_prb. aw; by constructor 2. move=> [Qxa Qyb]. case: hy; move => [pya qya]; first by case: Qyb. case: hx; move => [pxa qxa]; last by case: nT; ue. move /candu2P: pya =>[_]; case; move => [sa sb]. constructor 1; rewrite /f; Ytac0; Ytac0; Ytac0; aw; split => //. apply /orsum2_gleP; split => //. - by apply candu2_pra. - by apply candu2_prb. - by constructor 3; aw. by constructor 3; rewrite /f sb; Ytac0; Ytac0; aw; Ytac0;aw. move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP. rewrite orsum2_sr // -/A -/B -/C - Ev;split => //. case: hx; move => [Px Qx]. have fx: f x = (J (J (P x) C0) C0) by rewrite /f Y_true. case: hy; move => [Py Qy]. have fy: f y = (J (J (P y) C0) C0) by rewrite /f Y_true. constructor 1; split => //. move: h; rewrite fx fy ! pr1_pair ! pr2_pair; case. - move=> [_ _] /orsum2_gleP [_ _]; case; aw; first by move => [_ _ s]. + by move=> [_ bad _]. + by move=> [_ bad]. - by move=> [_ bad _]. - by move=> [_ bad]. constructor 3; rewrite Qx Qy; split; exact. case: hy; move => [Py Qy]. case: (nT); case: h. move=> [Qfx Qfy] /orsum2_gleP [Pfx Pfy]. have -> : Q (P (f y)) = C0 by rewrite /f; Ytac0; aw. case; [ | move => [_ pa _] | move => [_ pa]]; try by case: pa. move=> [h1 _]; move: h1 Qfx; rewrite /f Qx (Y_false) //;Ytac ww; aw. by move => [_ pa _]; move: pa; rewrite /f; Ytac0; aw. by move => [ _ ]; rewrite /f; Ytac0; aw. rewrite Qx Qy; constructor 2; split => //. apply /orsum2_gleP; split => //. move: Px Py => /candu2P [pPx hpx] /candu2P [pPy hpy]. case: hpx; move => [pa pb]. case: hpy; move => [pc pd]; last by constructor 3; rewrite pd;split => //. constructor 1; split => //; move: h; rewrite /f Qx Qy; do 4 Ytac0. case; [move => [_ _ ba] | move => [ba _] | move=> [_ ba]]; move: ba; aw => //. move /orsum2_gleP => [_ _];rewrite !pr1_pair !pr2_pair. by case; [ move => [sa _] | move => [_ _] | move => [sa _]]. constructor 2; rewrite pb; move: h; rewrite /f Qx Qy pb. Ytac0; Ytac0; Ytac0; case; first by move => [sa _]; move: sa; aw. Ytac ww; first by move => [_ qa _]; move: qa; aw. by move => [_ _]; aw. by move => [sa _]; move: sa; aw. Qed. Lemma oprod_assoc2 a b c: order a -> order b -> order c -> (order_prod2 a (order_prod2 b c)) \Is (order_prod2 (order_prod2 a b) c). Proof. move=> oa ob oc. have oab: order (order_prod2 a b) by fprops. have obc: order (order_prod2 b c) by fprops. set E:= substrate (order_prod2 a (order_prod2 b c)). set F:= substrate (order_prod2 (order_prod2 a b) c). set A:= substrate a; set B := substrate b; set C := substrate c. have Ev: E = product2 (product2 C B) A. by rewrite /E ! orprod2_sr. have Fv: F = product2 C (product2 B A). by rewrite /F ! orprod2_sr. have CB_pr: forall z, inc z (product2 C B) <-> [/\ fgraph z, domain z = C2, inc (Vg z C0) C & inc (Vg z C1) B]. by move=> z; apply /setX2_P. have BA_pr: forall z, inc z (product2 B A) <-> [/\ fgraph z, domain z = C2, inc (Vg z C0) B & inc (Vg z C1) A]. by move=> z; apply /setX2_P. set f := fun z => variantLc (Vg (Vg z C0) C0) (variantLc (Vg (Vg z C0) C1) (Vg z C1)). have p01: forall x, inc x E -> inc (f x) F. move=> x; rewrite Ev Fv; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3]. rewrite /f; bw; apply /setX2_P; split => //; fprops; bw. apply /setX2_P; split => //; fprops; bw. have p02: forall x y, inc x E -> inc y E -> f x = f y -> x = y. move=> x y; rewrite Ev; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3]. rewrite /f; move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3'] sf. move: (f_equal (Vg ^~ C0) sf) (f_equal (Vg ^~C1) sf); bw => sf1 sf2. move: (f_equal (Vg ^~C0) sf2) (f_equal (Vg ^~C1) sf2); bw => sf3 sf4. apply: fgraph_exten =>//; try ue. rewrite p2; move=> z zdx;try_lvariant zdx. apply: fgraph_exten =>//; try ue. rewrite p5; move=> zz zdx; try_lvariant zdx. have p03: forall y, inc y F -> exists2 x, inc x E & y = f x. move=> y; rewrite Fv; move /setX2_P => [p1 p2 p3 /setX2_P [p4 p5 p6 p7]]. exists (variantLc (variantLc (Vg y C0) (Vg (Vg y C1) C0)) (Vg (Vg y C1) C1)). rewrite Ev;apply /setX2_P; split;fprops; bw. apply /setX2_P; split;fprops; bw. rewrite /f; symmetry;apply: fgraph_exten => //; bw; fprops. move=> x xtp; try_lvariant xtp. apply: fgraph_exten => //; bw ; [fprops | by symmetry | ]. move=> z xtp; try_lvariant xtp. exists (Lf f E F); split => //; fprops;aw. split; aw;apply: lf_bijective => //. red; aw; move=> x y xE yE; aw. move: (xE); rewrite Ev;move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3]. move: (yE);rewrite Ev;move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3']. split. move: (p01 _ xE)(p01 _ yE) => xF yF. move: xF; rewrite Fv; case /setX2_P=>[q1 q2 q3 /setX2_P [q4 q5 q6 q7]]. move: yF; rewrite Fv; case /setX2_P=>[r1 r2 r3 /setX2_P [r4 r5 r6 r7]]. have x1: inc (Vg (f x) C1) (product2 B A) by rewrite BA_pr. have y1: inc (Vg (f y) C1) (product2 B A) by rewrite BA_pr. set hi1:= inc (Vg (f x) C1) (product2 B A). set hi2:= inc (Vg (f y) C1) (product2 B A). move => tmp; apply /(orprod2_gleP oab oc). rewrite orprod2_sr // -/A -/B -/C -Fv;split => //; try apply: p01 => //. move: tmp => /(orprod2_gleP oa obc) [_ _]; case. move => [pa pb];left; split; first by rewrite /f; bw;ue. apply /(orprod2_gleP oa ob);split => //;left. by rewrite /f; bw;split => //; rewrite pa. move => [] /(orprod2_gleP ob oc) [_ _ aux'] nse. case: aux'; last by move=> aux2; right; rewrite /f; bw. move=> [Vaa Vba]; left; split; first by rewrite /f; bw. apply /(orprod2_gleP oa ob);split => //; right. rewrite /f; bw; split => //; dneg aux3. apply: fgraph_exten =>//; try ue. rewrite p5; move=> z zd; try_lvariant zd. move /(orprod2_gleP oab oc) => [_ _ tmp]. apply/(orprod2_gleP oa obc); rewrite orprod2_sr // -/A -/B -/C -Ev;split => //. have x1: inc (Vg x C0) (product2 C B) by rewrite CB_pr. have y1: inc (Vg y C0) (product2 C B) by rewrite CB_pr. case: tmp; last first. rewrite /f; bw; move=> [h1 h2]; right; split. apply /(orprod2_gleP ob oc);split => //; by right. by dneg eql; rewrite eql. rewrite /f; bw; move => [xaa] /(orprod2_gleP oa ob) [fxb fxa]; bw. case. move=> [sVab le]; left; split =>//. apply: fgraph_exten => //; first by ue. rewrite p5; move=> z zd; try_lvariant zd. move=> [lt2 neq]; right;split; last by dneg aux; rewrite aux. by apply /(orprod2_gleP ob oc);split => //; left. Qed. Lemma osum_distributive a b c: order a -> order b -> order c -> (order_prod2 c (order_sum2 a b)) \Is (order_sum2 (order_prod2 c a) (order_prod2 c b)). Proof. move=> oa ob oc. move: (orsum2_or oa ob) => oab. move: (orprod2_or oc oa) => oca. move: (orprod2_or oc ob) => ocb. move: (orprod2_or oc oab) => ocab. move:(orsum2_or oca ocb) => ocacb. set (f := fun z => J (variantLc (P (Vg z C0)) (Vg z C1)) (Q (Vg z C0))). set A := substrate a; set B := substrate b; set C := substrate c. set E:= substrate (order_prod2 c (order_sum2 a b)). set F:= substrate(order_sum2 (order_prod2 c a)(order_prod2 c b)). have Ep: E = product2 (canonical_du2 A B) C. rewrite /E orprod2_sr // orsum2_sr //. have Fp: F = canonical_du2 (product2 A C)(product2 B C). rewrite /F orsum2_sr // !orprod2_sr //. have Ev: forall x, inc x E <-> [/\ fgraph x, domain x = C2, pairp (Vg x C0), ((inc (P (Vg x C0)) A /\ Q (Vg x C0) = C0) \/ (inc (P (Vg x C0)) B /\ Q (Vg x C0) = C1)) &inc (Vg x C1) C]. move=> x; rewrite Ep; split. move /setX2_P => [pa pb pc pd]; move/candu2P: pc => [pe] [] [pf pg]; split => //; [left | right ]; split => //. by move => [pa pb pc pd pe]; apply /setX2_P;split => //; apply/candu2P. have Fv: forall x, inc x F <-> [/\ pairp x, fgraph (P x), domain (P x) = C2, inc (Vg (P x) C1) C & ((inc (Vg (P x) C0) A /\ Q x = C0) \/ (inc (Vg (P x) C0) B /\ Q x = C1))]. move=> x; rewrite Fp; split. move /candu2P => [pa []] [] /setX2_P [pb pc pd pe] pf; split;fprops. move => [pa pb pc pd];case; move =>[pe pf]; apply /candu2P;split => //; [left | right]; split => //;apply /setX2_P; split; fprops. have p1: forall x, inc x E -> inc (f x) F. move=> x /Ev [pa pb pc pd pe]; rewrite /f; apply/Fv. rewrite !pr1_pair !pr2_pair; bw; split;fprops. have p2: forall x y, inc x E -> inc y E -> f x = f y -> x = y. move=> x y /Ev [fgx dx px hx qx] /Ev [fgy dy py hy qy]. rewrite /f => sf; move: (pr1_def sf)(pr2_def sf) => r1 r2. move: (f_equal (Vg ^~C0) r1)(f_equal (Vg ^~C1) r1); bw; move => r3 r4. apply: fgraph_exten =>//; [ ue | rewrite dx; move=> z zd; try_lvariant zd]. apply: pair_exten =>//. have p3: forall y, inc y F -> exists2 x, inc x E & y = f x. move=> y /Fv [py fPy dPy Vby Vay]. exists (variantLc (J (Vg (P y) C0) (Q y)) (Vg (P y) C1)). apply /Ev; bw; rewrite !pr1_pair !pr2_pair; split;fprops. rewrite /f; bw;aw; apply: pair_exten =>//; [ fprops | aw | aw]. apply: fgraph_exten; [ exact| fprops | bw | bw]. rewrite dPy; move=> x xtp; try_lvariant xtp. exists (Lf f E F); split => //; aw; first by split; aw;apply: lf_bijective. red; aw;move=> x y xE yE; rewrite lf_V // lf_V //. have r1: Q (f x) = Q (Vg x C0) by rewrite /f pr2_pair. have r2: Q (f y) = Q (Vg y C0) by rewrite /f pr2_pair. have r3: Vg (P (f x)) C0 = P (Vg x C0) by rewrite /f; aw; bw. have r4: Vg (P (f y)) C0 = P (Vg y C0) by rewrite /f; aw; bw. have r5: Vg (P (f x)) C1 = Vg x C1 by rewrite /f; aw; bw. have r6: Vg (P (f y)) C1 = Vg y C1 by rewrite /f; aw; bw. have pa: pairp (Vg x C0) by move /Ev: xE => [_ _ px _]. have pb: pairp (Vg y C0) by move /Ev:yE => [_ _ px _]. move: (xE) => /Ev [fgx dx px hx qx]. move: (yE) => /Ev [fgy dy py hy qy]. move: C0_ne_C1 => nab. split. move /(orprod2_gleP oc oab) => [_ _ h]; apply /(orsum2_gleP). split; first by move: (p1 _ xE); rewrite /F orsum2_sr. by move: (p1 _ yE); rewrite /F orsum2_sr. rewrite r1 r2; case: h. move=> [q1 q2]; rewrite -q1. case: (equal_or_not (Q (Vg x C0)) C0)=> q3. case: hx; move=> [q4 q5]; last by case: nab ; rewrite - q3 - q5. constructor 1; rewrite q3; split => //. apply /(orprod2_gleP oc oa). split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops. by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops; ue. left; rewrite r3 r4 r5 r6 q1; split =>//. constructor 2; split => //. case: hx; move=> [q4 q5]; first by case: q3. apply /(orprod2_gleP oc ob). split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops. by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops; ue. left; rewrite r3 r4 r5 r6 -q1; split =>//. move => [] /(orsum2_gleP) [_ _ h1] h2; case: h1. move=> [q1 q2 q3]; constructor 1. split; [exact | exact | ]. case: hx; move=> [q4 q5]; last by case: nab; rewrite -q1 -q5. case: hy; move=> [q4' q5']; last by case: nab; rewrite -q2 -q5'. apply /(orprod2_gleP oc oa). split; first by apply/setX2_P; rewrite /f pr1_pair; bw; split;fprops. by apply/setX2_P; rewrite /f pr1_pair; bw; split;fprops. right; rewrite r3 r4;split => //;dneg aux. apply: pair_exten => //; ue. move => [q1 q2 q3]; constructor 2. case: hx; move=> [q4 q5]; first by case: q1. case: hy; move=> [q4' q5']; first by case: q2. split; [exact | exact | ]. apply /(orprod2_gleP oc ob). split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops. by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops. right; rewrite r3 r4; split => // sP; case: h2. by apply: pair_exten => //; rewrite q5 q5'. move=> res; constructor 3; exact. move/(orsum2_gleP) => [_ _ h]; apply /(orprod2_gleP oc oab). split; first by move: xE; rewrite /E orprod2_sr //. by move: yE; rewrite /E orprod2_sr //. have pc: inc (Vg x C0) (canonical_du2 (substrate a) (substrate b)). by move: xE => /Ev [_ _ px' etc _]; apply/candu2P. have pd: inc (Vg y C0) (canonical_du2 (substrate a) (substrate b)). by move: yE => /Ev [_ _ px' etc _]; apply/candu2P. case: h. move=> [q1 q2] /(orprod2_gleP oc oa) [q3 q4]. rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ]. by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 q1 q2. split =>//; last by dneg neq; rewrite neq. by apply /orsum2_gleP;split => //; constructor 1;rewrite -r1 -r2 q1 q2. move=> [q1 q2] /(orprod2_gleP oc ob) [q3 q4]. case: hx; rewrite -r1; move => [_ sb]; first by case: q1. case: hy; rewrite -r2; move => [_ sb']; first by case: q2. rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ]. by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 sb sb'. split =>//; last by dneg neq; rewrite neq. apply /orsum2_gleP;split => //; constructor 2; rewrite - r1 -r2;split => //. move=> [q5 q6]; right; split. apply /orsum2_gleP;split => //; constructor 3; rewrite - r1 -r2;split => //. by dneg neq; rewrite r2 -neq -r1. Qed. Lemma osum_increasing1 r f g: orsum_ax r f -> orsum_ax r g -> (forall x, inc x (domain f) -> order_le (Vg f x) (Vg g x)) -> order_le (order_sum r f) (order_sum r g). Proof. move => oa oa1 ale. have o1: order (order_sum r f) by fprops. have o2: order (order_sum r g) by fprops. split => //; apply: (proj33 (order_le_alt o1 o2 _)). set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)). have sip: forall j, inc j (domain f) -> order_morphism (si j) (Vg f j) (Vg g j). move=> j jdf; move:(ale _ jdf) => [p1 p2 [f0 [x [ fx1 fx2]]]]. move: (order_le_alt2 p1 p2 fx1 fx2) => [res _]. rewrite /si; apply choose_pr. by exists (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))). have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue. set E := (substrate (order_sum r g)). set F := (disjointU_fam (fam_of_substrates f)). have p1: partition_w_fam F (substrate (order_sum r f)). bw;rewrite /F /sum_of_substrates; rewrite /disjointU. apply: partition_disjointU; rewrite /fam_of_substrates; fprops. have p3: (domain F = domain f). rewrite /F/disjointU_fam /fam_of_substrates; bw. set di:= fun i => ((substrate (Vg f i)) *s1 i). set sj:= fun i => Lf (fun z => J (Vf (si i) (P z)) i) (di i) E. have p0: forall i, inc i (domain f) -> lf_axiom (fun z => J (Vf (si i) (P z)) i) (di i) E. move=> i idf z zV. move: (sip _ idf) => [_ _ [ff sf tf] _]. have aux: inc (Vf (si i) (P z) ) (substrate (Vg g i)). Wtac;move: zV => /indexed_P [_ Ps _]; ue. rewrite /E;bw; apply: disjoint_union_pi1 => //; ue. have FP: forall i, inc i (domain f) -> Vg F i = di i. move=> i idf; rewrite /F /disjointU_fam/fam_of_substrates ; bw. have p2: forall i, inc i (domain F) -> function_prop (sj i) (Vg F i) E. rewrite p3;move=> i idf; rewrite /sj FP => //; aw. by split;aw;apply: lf_function; apply: p0. move: (extension_partition1 p1 p2). set G := common_ext _ _ _; move=> [[fG sG tG] alg]. rewrite p3 in alg. have aux: forall x, inc x (source G) -> [/\ inc (Q x) (domain f), inc x (di (Q x)), pairp x, inc (P x)(substrate (Vg f (Q x))) & Vf G x = J (Vf(si (Q x)) (P x)) (Q x)]. rewrite sG; bw; move => x xs; move: (du_index_pr1 xs)=> [Qxd Pxd px]. have xdi: inc x (di (Q x)) by apply /indexed_P;split => //. split => //. move: (alg _ Qxd); rewrite /agrees_on; move=> [q1 q2 q3]. move: (xdi); rewrite -FP // => q4. move: (q3 _ q4); rewrite /sj; rewrite lf_V; aw;apply: p0 => //. exists G; split => //. move=> x y xs ys. move: (aux _ xs) (aux _ ys) => [Qx xdi px Px Wx][Qy ydi py Py Wy]. have qa: (sum_of_substrates f = source G) by rewrite sG; bw. have qb: (sum_of_substrates g = target G) by rewrite tG /E; bw. split; move /orsum_gleP =>[q1 q2 q3]; apply /orsum_gleP. rewrite qb;split=> //; try Wtac; rewrite Wx Wy;red;aw; case: q3; first by left. move=> [Qxx le1]; right; split => //. rewrite -Qxx; move: (sip _ Qx) => [_ _ [_ sf tf] orf]. rewrite - orf //; rewrite sf //; ue. move: q3; rewrite /order_sum_r Wx Wy !pr2_pair !pr1_pair. move => q3; rewrite qa;split => //; case: q3; first by left. move=> [Qxx]; rewrite - {1} Qxx => le1; right; split => //. move: (sip _ Qx) => [_ _ [_ sf tf] orf]. apply /orf; rewrite ? sf //; ue. Qed. Lemma osum_increasing2 r f g: worder r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) -> (osum r f) <=o (osum r g). Proof. move=> wor sf sg alo. have ha: worder_on r (domain g) by []. have hb: worder_on r (domain f) by []. apply /ordinal_le_P0; apply /order_le_compatible1. apply: orsum_wor => //; bw. hnf; bw;move=> i idf; bw; fprops; move: (alo _ idf) => [aa bb _]; fprops. apply: orsum_wor => //;bw. hnf; bw;rewrite - sg sf; move=> i idf; bw. move: (alo _ idf) => [aa bb _]; fprops. apply osum_increasing1. - split => //;bw; fprops; hnf; bw. move=> i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops. - rewrite - sg sf;split;fprops;hnf; bw. move=> i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops. - rewrite - sg sf; bw => x xdf; move: (alo _ xdf) =>[aa bb le]. bw; apply/order_le_compatible1; fprops. by rewrite (ordinal_o_o aa) (ordinal_o_o bb) ; apply/ordinal_le_P0. Qed. Lemma osum_increasing3 r f j: orsum_ax r f -> sub j (domain f) -> order_le (order_sum (induced_order r j) (restr f j)) (order_sum r f). Proof. move=> oa jd. move: (oa) => [or sr alo]. set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) emptyset)). have dfdg: domain f = domain g by rewrite /g; bw. have oa': orsum_ax r g. split => //; first by ue. hnf;bw;rewrite - dfdg /g;move=> i idg; bw; Ytac ij;first by apply: alo. apply: set0_or. have sjd': sub j (domain g) by ue. have cz: (forall i, inc i ((domain g) -s j) -> Vg g i = \0o). by move=> i /setC_P; rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0. move: (osum_unit1 oa' sjd' cz). have ->: (restr f j = restr g j). apply: Lg_exten => s sj;bw; rewrite /g; bw; [ by Ytac0 | by apply:jd ]. move=> oi1. have oi2: order_isomorphic (order_sum r f) (order_sum r f). by apply: orderIR; apply: orsum_or. apply /(order_le_compatible oi1 oi2). apply: osum_increasing1 => //. rewrite -dfdg; move=> x xdg; rewrite /g; bw. Ytac xj; first by apply: order_leR=>//; apply: alo. move: set0_or => eo. split; fprops;exists (identity emptyset); exists emptyset. have auw: sub emptyset (substrate (Vg f x)) by fprops. split => //; split;fprops; aw. - apply: (proj1 (iorder_osr _ auw)); fprops. split; aw; first by apply: identity_fb. by rewrite (proj2 set0_wor). - apply: (alo _ xdg). - by move=> u v; rewrite identity_s => /in_set0. Qed. Lemma osum_increasing4 r f j: worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f -> (osum (induced_order r j) (restr f j)) <=o (osum r f). Proof. move => [wor sr] sjf alo. have sjr: sub j (substrate r) by ue. have or: order r by move: wor => [or _]. have dr: (domain (restr f j)) = j by bw. have ha:worder_on r (domain f) by []. rewrite /osum; apply /ordinal_le_P0; apply /order_le_compatible1. apply: orsum_wor. by split;[ apply: induced_wor => //; ue | bw; aw;rewrite dr]. by hnf; rewrite dr; bw; move=> i ij; bw; fprops. apply: orsum_wor => //; hnf; bw; move=> i idf; bw; fprops. set g:= (Lg (domain f) (fun z : Set => ordinal_o (Vg f z))). have ->: (Lg (domain (restr f j)) (fun z => ordinal_o (Vg (restr f j) z))) = restr g j. bw;apply: Lg_exten. by rewrite /g;red; bw;move => x xj; bw; apply: sjf. apply: osum_increasing3 => //. rewrite /g;red; bw;split => //; hnf;bw; move=> i idf; bw; fprops. rewrite /g; bw. Qed. Lemma oprod_increasing1 r f g: orprod_ax r f -> orprod_ax r g -> (forall x, inc x (domain f) -> order_le (Vg f x) (Vg g x)) -> order_le (order_prod r f) (order_prod r g). Proof. move => oa oa1 ale. have o1: order (order_prod r f) by fprops. have o2: order (order_prod r g) by fprops. split => //; apply: (proj33 (order_le_alt o1 o2 _)). set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)). have sip: forall j, inc j (domain f) -> order_morphism (si j) (Vg f j) (Vg g j). move=> j jdf; move:(ale _ jdf) => [p1 p2 [f0 [x [fx1 fx2]]]]. move: (order_le_alt2 p1 p2 fx1 fx2) => [res _]. rewrite /si; apply choose_pr. by exists (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))). have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue. set E:= substrate (order_prod r f). set F := substrate(order_prod r g). have Ep: E = (prod_of_substrates f) by apply: orprod_sr => //. have Fp: F = (prod_of_substrates g) by apply: orprod_sr => //. set h:= fun z => Lg (domain f) (fun i => Vf (si i) (Vg z i)). have ta: lf_axiom h E F. rewrite Ep Fp ; move => t /prod_of_substratesP [fgt dt als]. apply /prod_of_substratesP. rewrite - dfdg /h; bw;split;fprops;move=> i idf; bw. move: (sip _ idf) => [_ _ [fsi ssi tsi] _]. by Wtac; rewrite ssi;apply: als. have hi: forall u v, inc u E -> inc v E -> h u = h v -> u = v. rewrite Ep; move=> u v / prod_of_substratesP [fgu du alu] /prod_of_substratesP [fgv dv alv] sh. apply: fgraph_exten =>//; first by ue. rewrite du; move=> x xdf; move: (f_equal (Vg ^~x) sh); rewrite /h;bw => sW. move: (order_morphism_fi (sip _ xdf)) => [_ insi]. move: (sip _ xdf) => [_ _ [fsi ssi tsi] _]. apply: insi =>//; rewrite ssi; [ apply: alu => // |apply: alv => //]. exists (Lf h E F); red; aw; split => //. split; aw;by apply: lf_function. red; aw; move=> x y xE yE; rewrite /h; aw. have srdf: substrate r = domain f by move: oa => [_ sr _]. move: (xE); rewrite Ep; move /prod_of_substratesP => [fgx dx alx]. move: (yE); rewrite Ep; move /prod_of_substratesP => [fgy dy aly]. split. move /(orprod_gleP oa) => [_ _ aux]; apply /(orprod_gleP oa1). rewrite -Fp;split; [by apply: ta | by apply: ta |]. case: aux; first by move=>->; left. move=> [j [jsr jlt jle]]; right; ex_tac. rewrite srdf in jsr;move: jlt; bw. move: (order_morphism_fi (sip _ jsr)) => [_ insi]. move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp]. have vsx: inc (Vg x j) (source (si j)) by rewrite ssi; apply: alx => //. have vsy: inc (Vg y j) (source (si j)) by rewrite ssi; apply: aly => //. rewrite /glt -jsrp //;move=> [p1 p2]; split =>//; dneg sV; apply: insi =>//. move=> i ij. have idf: inc i (domain f) by rewrite - srdf; order_tac. by move: (jle _ ij); bw; move=> ->. move /(orprod_gleP oa1) => [h1 h2 aux]; apply /(orprod_gleP oa). rewrite -Ep; split=> //; case: aux. move => sh; left; apply: hi =>//. move=> [j [jsr jlt jle]]; right; ex_tac. rewrite srdf in jsr;move: jlt; bw. move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp]. rewrite /glt jsrp; first by move=> [p1 p2]; split =>//; dneg sV; ue. rewrite ssi; apply: alx => //. rewrite ssi; apply: aly => //. move=> i ij. have idf: inc i (domain f) by rewrite - srdf; order_tac. move: (jle _ ij); bw. move: (order_morphism_fi (sip _ idf)) =>[_ insi]. move: (sip _ idf) => [_ _ [fsi ssi tsi] jsrp]. apply: insi; rewrite ssi;[ apply: alx => // | apply: aly => //]. Qed. Lemma oprod_increasing2 r f g: worder r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) -> finite_set (substrate r) -> (oprod r f) <=o (oprod r g). Proof. move=> wor sf sg alo fse. apply/ordinal_le_P0; apply /order_le_compatible1. apply: orprod_wor => //; [ split;bw | hnf; bw ]. move=> i idf; bw; move: (alo _ idf) => [aa bb _]; fprops. apply: orprod_wor => //; [split; bw | hnf;bw ]. rewrite - sg sf; move=> i idf; bw. by move: (alo _ idf) => [aa bb _]; fprops. apply: oprod_increasing1. split => //;bw; hnf; bw => i idf; bw;move: (alo _ idf) =>[aa bb _];fprops. split => //; bw; hnf; bw; rewrite - sg sf. move => i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops. rewrite - sg sf; bw => x xdf; move: (alo _ xdf) =>[aa bb le]. bw; apply /order_le_compatible1; fprops. by rewrite (ordinal_o_o aa) (ordinal_o_o bb); apply/ordinal_le_P0. Qed. Lemma oprod_increasing3 r f j: orprod_ax r f -> sub j (domain f) -> (forall x, inc x ((domain f) -s j) -> substrate (Vg f x) <> emptyset) -> order_le (order_prod (induced_order r j) (restr f j)) (order_prod r f). Proof. move=> oa jd anot. move: (oa) => [or sr alo]. set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) (ordinal_o \1o))). have dfdg: domain f = domain g by rewrite /g; bw. have oa': orprod_ax r g. hnf; rewrite /order_fam /allf - dfdg;split => //. move=> i idg; rewrite /g; bw; Ytac ij; first by apply: alo. by apply: (ordinal_o_or). have sjd': sub j (domain g) by ue. have cz: (forall i, inc i ((domain g) -s j) -> singletonp (substrate (Vg g i))). move=> i /setC_P;rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0. by rewrite (ordinal_o_sr); exists emptyset. move: (oprod_unit1 oa' sjd' cz). have ->: (restr f j = restr g j). apply: Lg_exten; bw; move=> x xj; move: (jd _ xj) => xdf. by bw; rewrite /g; bw; Ytac0. move=> oi1. have oi2: order_isomorphic (order_prod r f) (order_prod r f). by apply: orderIR; apply: orprod_or. apply /(order_le_compatible oi1 oi2). apply: oprod_increasing1 => //. rewrite -dfdg; move=> x xdg; rewrite /g; bw. Ytac nij; first by apply: order_leR=>//; apply: alo. have p2: order (Vg f x) by move: oa => [q1 q2 q4]; apply: q4. have [y yd]: nonempty (substrate (Vg f x)). case: (emptyset_dichot (substrate (Vg f x))) => // p1. have xcz: inc x ((domain f) -s j) by apply /setC_P. move: (anot _ xcz) => p4; contradiction. have s1: sub (singleton y) (substrate (Vg f x)) by apply: set1_sub. set h:= Lf (fun z => y) (singleton emptyset) (singleton y). have ta: lf_axiom (fun _ : Set => y) (singleton emptyset) (singleton y). move=> t _ /=; fprops. split => //; [fprops | exists h; exists (singleton y); split => //]. rewrite /h;split;fprops;bw; aw. apply (proj1 (iorder_osr p2 s1)). split; rewrite ? ordinal_o_sr;aw; apply: lf_bijective => //. by move=> u v /set1_P -> /set1_P ->. move=> u /set1_P ->; exists emptyset; [fprops | done]. move => u v;rewrite lf_source => aa bb; aw. move: aa bb => /set1_P -> /set1_P ->. split; move => _. by apply /iorder_gleP; fprops; order_tac. rewrite / \1o/ \1c;apply /ordo_leP;split;fprops. Qed. Lemma oprod_increasing4 r f j: worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f -> finite_set (substrate r) -> (forall x, inc x ((domain f) -s j) -> Vg f x <> \0o) -> (oprod (induced_order r j) (restr f j)) <=o (oprod r f). Proof. move => [wor sr] sjf alo fsr alnz. have sjr: sub j (substrate r) by ue. have or: order r by move: wor => [or _]. apply /ordinal_le_P0; apply /order_le_compatible1. apply: orprod_wor. split; bw;aw; apply: induced_wor => //; ue. hnf; bw; move=> i ij; bw; fprops. rewrite iorder_sr //; apply: (sub_finite_set sjr fsr). apply: orprod_wor => //; [ split;bw | hnf;bw ]. move=> i idf; bw; fprops. set g:= (Lg (domain f) (fun z : Set => ordinal_o (Vg f z))). have ->: (Lg (domain (restr f j)) (fun z => ordinal_o (Vg (restr f j) z))) = restr g j. bw;apply: Lg_exten; rewrite /g; bw. by move => x xj /=; bw;apply: sjf. apply: oprod_increasing3 => //. rewrite /g;split=> //;hnf; bw; move=> i idf; bw; fprops. rewrite /g; bw. move => x; rewrite {1} /g; bw => xd; move: (alnz _ xd). move: xd => /setC_P [xdf _]; move: (alo _ xdf) => ov. by rewrite /g; bw; rewrite ordinal_o_sr. Qed. Lemma cardinal_du2 A B : cardinal (canonical_du2 A B) = (cardinal A) +c (cardinal B). Proof. rewrite /canonical_du2 csum_pr /csumb; bw. have c0C2: inc C0 C2 by rewrite /C2; fprops. have c1C2: inc C1 C2 by rewrite /C2; fprops. set f := Lg C2 _. have df: doubleton_fam f (cardinal A) (cardinal B). exists C0, C1; rewrite /f; split;fprops; bw. by rewrite - (csum2_pr df). Qed. Parameter order_type_of: Set -> Set. Axiom order_type_exists: forall x, order x -> order_isomorphic x (order_type_of x). Axiom order_type_unique: forall x y, order_isomorphic x y -> (order_type_of x = order_type_of y). Definition order_type x := exists2 y, order y & x = order_type_of y. Definition order_type_le x y:= [/\ order_type x, order_type y & exists f z, sub z (substrate y) /\ order_isomorphism f x (induced_order y z)]. Notation "x <=t y" := (order_type_le x y) (at level 60). Notation "x <=O y" := (order_le x y) (at level 60). Lemma OT_ordinal_compat x: worder x -> order_type_of x = order_type_of (ordinal_o (ordinal x)). Proof. by move=> wor; apply: order_type_unique;move:(ordinal_o_is wor). Qed. Lemma OT_prop0 x: order x -> (order_type_of x) \Is x. Proof. by move=> ox; apply: orderIS; apply: order_type_exists. Qed. Lemma OT_prop1 x: order x -> order_type (order_type_of x). Proof. by move=> ox; exists x. Qed. Lemma OT_prop2 x: order_type x -> order x. Proof. move=> [y pa pb]. by move: (order_type_exists pa); rewrite -pb; move=> [f [oy ox _]]. Qed. Lemma OT_prop3 x: order x -> order (order_type_of x). Proof. by move => ox; apply: OT_prop2; apply: OT_prop1. Qed. Lemma OT_prop4 x: order x -> order_type_of (order_type_of x) = order_type_of x. Proof. move => ox. by apply: order_type_unique; apply: orderIS; apply: order_type_exists. Qed. Lemma order_le_alt4 r r': r <=O r' -> (exists f, order_morphism f r r'). Proof. move=> [o1 o2 [f [z [sr [oa ob [[ [ff injf] sjf] sf tf] etc]]]]]. move: tf; aw => tf. have ta: lf_axiom (Vf f) (substrate r) (substrate r'). rewrite - sf; move=> t tsf; apply: sr; Wtac. exists (Lf (Vf f) (substrate r) (substrate r')). split => //;first split;aw. by apply: lf_function. red; aw;move=> x y xsr ysr; aw; rewrite - sf in xsr ysr. split => h; first by move/(etc _ _ xsr ysr): h => t; exact (iorder_gle1 t). apply /(etc _ _ xsr ysr); apply /iorder_gleP => //; Wtac. Qed. Lemma order_le_alt3P r r': r <=O r' <-> (exists f, order_morphism f r r'). Proof. split. apply: order_le_alt4. move => h; move: (h) => [_ [or or' _ _]]. by apply: order_le_alt. Qed. Lemma order_le_transitive x y z: x <=O y -> y <=O z -> x <=O z. Proof. move=> [ox oy [f [y1 [pa pb]]]] [_ oz [g [z1 [pc pd]]]]. split => //. move: pb => [orx oix [[[ff injf] sjf] sf tf] etcf]. move: pd => [ory oiy [[[fg injg] sjg] sg tg] etcg]. move: tf tg; aw => tf tg. set z2:= Vfs g y1. have y1sg: sub y1 (source g) by ue. have sz2z1: sub z2 z1 by rewrite - tg /z2; apply: fun_image_Starget1. have sz2: sub z2 (substrate z) by apply: (sub_trans sz2z1). set h:= Lf (fun t => (Vf g (Vf f t))) (substrate x) z2. have ta: lf_axiom (fun t => Vf g(Vf f t)) (substrate x) z2. rewrite - sf;move=> t rx; apply /(Vf_image_P fg y1sg). exists (Vf f t) => //; Wtac. move: (iorder_osr oz sz2) => [pa1 pb1]. exists h; exists z2; split => //; rewrite /h; split;fprops;aw. split; aw;apply: lf_bijective => //. rewrite - sf => u v ux vx sw; apply: injf => //. apply: injg =>//; rewrite sg; apply: pa; rewrite - tf;Wtac. move=> u /(Vf_image_P fg y1sg) [a ay1] ->. move: ay1; rewrite - tf => af; move: ((proj2 sjf) _ af). move=> [b bsf <-]; exists b => //; ue. red; aw;move => a b asf bsf. move: (ta _ asf) (ta _ bsf) => ta1 ta2; aw. rewrite - sf in asf bsf. have wa: inc (Vf f a) y1 by rewrite - tf; Wtac. have wb: inc (Vf f b) y1 by rewrite - tf; Wtac. have wa1: inc (Vf f a) (source g) by ue. have wb1: inc (Vf f b) (source g) by ue. set H1 := (etcf _ _ asf bsf); set Hb := (etcg _ _ wa1 wb1). split. move /H1 => p1; apply /iorder_gleP => //. move: (iorder_gle1 p1); move /Hb => p2; exact :(iorder_gle1 p2). move => p2; apply /H1;apply /iorder_gleP => //; apply /Hb. move: (iorder_gle1 p2) => p1. by apply /iorder_gleP => //; apply: sz2z1. Qed. Lemma OTorder_le_altP r r': r <=t r' <-> [/\ order_type r, order_type r' & exists f, order_morphism f r r']. Proof. split;move=> [o1 o2 etc]; split => //. apply /order_le_alt3P. by split => //; by apply: OT_prop2. by move: (order_le_alt (OT_prop2 o1)(OT_prop2 o2) etc) => [_ _]. Qed. Lemma OTorder_le_compat1 r: order r -> r <=O (order_type_of r). Proof. move=> or; apply /order_le_alt3P. move: (order_type_exists or) => [f oi]; exists f => //. by apply: order_isomorphism_w. Qed. Lemma OTorder_le_compat2 r: order r -> (order_type_of r) <=O r. Proof. move=> or; apply /order_le_alt3P. move: (OT_prop0 or) => [f oi]; exists f => //. by apply: order_isomorphism_w. Qed. Lemma OTorder_le_compatP r r': order r -> order r' -> (r <=O r' <-> (order_type_of r) <=O (order_type_of r')). Proof. move=> or or'. split => h. apply: (@order_le_transitive _ r). apply: OTorder_le_compat2 => //. apply: (@order_le_transitive _ r') => //. apply: OTorder_le_compat1 => //. apply: (@order_le_transitive _ (order_type_of r)). apply: OTorder_le_compat1 => //. apply: (@order_le_transitive _ (order_type_of r')) => //. apply: OTorder_le_compat2 => //. Qed. Lemma OT_order_le_reflexive x: order_type x -> x <=t x. Proof. move=> ox; split => //; exists (identity (substrate x)); exists (substrate x). split; first by fprops. move: (OT_prop2 ox) => orx. rewrite (iorder_substrate orx); exact: (identity_is orx). Qed. Lemma OTorder_le_alt2P r r': r <=t r' <-> [/\ order_type r, order_type r' & r <=O r']. Proof. split; first by move /OTorder_le_altP => [pa pb /order_le_alt3P pc]. by move => [pa pb /order_le_alt3P pc]; apply /OTorder_le_altP. Qed. Lemma OT_order_le_transitive x y z: x <=t y -> y <=t z -> x <=t z. Proof. move /OTorder_le_alt2P => [pa pb pc] /OTorder_le_alt2P [pd pe pf]. apply /OTorder_le_alt2P. split => //; apply: (order_le_transitive pc pf). Qed. Definition OT_sum r g := order_type_of (order_sum r (Lg (domain g) (fun z => (order_type_of (Vg g z))))). Definition OT_prod r g := order_type_of (order_prod r (Lg (domain g) (fun z => (order_type_of (Vg g z))))). Definition OT_sum2 a b := order_type_of (order_sum2 (order_type_of a) (order_type_of b)). Definition OT_prod2 a b := order_type_of (order_prod2 (order_type_of a) (order_type_of b)). Notation "x +t y" := (OT_sum2 x y) (at level 50). Notation "x *t y" := (OT_prod2 x y) (at level 40). Lemma OT_sum2_pr a b: a +t b = OT_sum canonical_doubleton_order (variantLc a b). Proof. rewrite /OT_sum2 /OT_sum /order_sum2. by rewrite variantLc_comp. Qed. Lemma OT_prod2_pr a b: a *t b = OT_prod canonical_doubleton_order (variantLc b a). Proof. rewrite /OT_prod2 /OT_prod /order_prod2. by rewrite variantLc_comp. Qed. Lemma OT_sum2_pr2 a b: order a -> order b -> OT_sum2 (order_type_of a) (order_type_of b) = order_type_of (order_sum2 a b). Proof. move => oa ob; symmetry. rewrite /OT_sum2 OT_prop4 // OT_prop4 //; apply: order_type_unique. by apply: orsum_invariant4; apply: order_type_exists. Qed. Lemma OT_prod2_pr2 a b: order a -> order b -> OT_prod2 (order_type_of a) (order_type_of b) = order_type_of (order_prod2 a b). Proof. move => oa ob; symmetry. rewrite /OT_prod2 OT_prop4 // OT_prop4 //; apply: order_type_unique. by apply: orprod_invariant4; apply: order_type_exists. Qed. Lemma OT_sum_ordertype r g: order r -> substrate r = domain g -> order_fam g -> order_type (OT_sum r g). Proof. move=> or sr alo; apply: OT_prop1. apply: orsum_or; bw; split => //; bw. by hnf; bw; move=> i idg; bw; apply: OT_prop3; apply: alo. Qed. Lemma OT_prod_ordertype r g: worder r -> substrate r = domain g -> order_fam g -> order_type (OT_prod r g). Proof. move=> or sr alo; apply: OT_prop1. apply: orprod_or; split => //; hnf;bw. by move=> i idg; bw;apply: OT_prop3; apply: alo. Qed. Lemma OT_sum2_ordertype a b: order_type a -> order_type b -> order_type (a +t b). Proof. move=> wo1 wo2;rewrite /OT_sum2; apply: OT_prop1. by apply: orsum2_or;apply: OT_prop3; apply: OT_prop2. Qed. Lemma OT_prod2_ordertype a b: order_type a -> order_type b -> order_type (a *t b). Proof. move=> wo1 wo2;rewrite /OT_prod2; apply: OT_prop1. by apply: orprod2_or; apply: OT_prop3; apply: OT_prop2. Qed. Lemma OT_sum_invariant3 r g: order r -> substrate r = domain g -> order_fam g -> order_type_of (order_sum r g) = OT_sum r (Lg (substrate r) (fun i => order_type_of (Vg g i))). Proof. move => or sr alo. rewrite /OT_sum;apply: order_type_unique. apply: orsum_invariant2; fprops;bw. rewrite sr;move=> i isr ; bw; move: (alo _ isr) => oi. by rewrite OT_prop4 //; apply: order_type_exists. Qed. Lemma OT_prod_invariant3 r g: worder r -> substrate r = domain g -> order_fam g -> order_type_of (order_prod r g) = OT_prod r (Lg (substrate r) (fun i => order_type_of (Vg g i))). Proof. move => or sr alo. rewrite /OT_prod;apply: order_type_unique. apply: orprod_invariant2;fprops;bw. rewrite sr;move=> i isr ; bw; move: (alo _ isr) => oi. by rewrite OT_prop4 //; apply: order_type_exists. Qed. Lemma OT_sum_invariant5 a b c: order a -> order b -> order c -> (order_sum2 a b) \Is c -> (order_type_of a) +t (order_type_of b) = order_type_of c. Proof. move=> oa ob oc => h. rewrite /osum2; apply: order_type_unique. rewrite OT_prop4 // OT_prop4 //. by apply: (@orderIT (order_sum2 a b)) => //; apply: orsum_invariant4;apply: OT_prop0. Qed. Lemma OT_prod_invariant5 a b c: order a -> order b -> order c -> (order_prod2 a b) \Is c -> (order_type_of a) *t (order_type_of b) = order_type_of c. Proof. move=> oa ob oc => h. rewrite /osum2; apply: order_type_unique. rewrite OT_prop4 // OT_prop4 //. by apply: (@orderIT (order_prod2 a b)) => //; apply: orprod_invariant4;apply: OT_prop0. Qed. Definition order_type_fam g := (allf g order_type). Lemma OT_sum_assoc1 r g r' g': order r -> substrate r = domain g -> order_type_fam g -> order r' -> substrate r' = domain g' -> order_fam g' -> r = order_sum r' g' -> let order_sum_assoc_aux := fun l => OT_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in OT_sum r g = OT_sum r' (Lg (domain g') (order_sum_assoc_aux)). Proof. move=> wor sr alB wor' sr' alw oal osa. rewrite /OT_sum. have oa': orsum_ax r' g' by []. apply: order_type_unique. set g'' := (Lg (domain g) (fun z => order_type_of (Vg g z))). have oa: orsum_ax r g''. rewrite /g'';red; bw; split => //;hnf;bw; move=> i idg; bw. by move: (OT_prop3 (OT_prop2 (alB _ idg))). move: (orsum_assoc_iso oa oa' oal) => /=. set aux' := fun l => order_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))). set f:= Lf _ _ _. move => oi1; move: (oi1) => [o1 o2 _ _]. apply: (@orderIT (order_sum r' (Lg (domain g') aux'))); first by exists f. apply: orsum_invariant2 =>//; bw; fprops. rewrite sr';move=> i isr; bw; rewrite /osa /OT_sum; bw. set s := order_sum _ _. have os: order s. rewrite /s; apply: orsum_or; split => //; bw; first by apply: alw. hnf; bw;move=> j js; bw. have jdg: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); apply: disjoint_union_pi1. apply: (OT_prop3 (OT_prop2 (alB _ jdg))). have -> : (aux' i = s). rewrite /aux' /s; apply: f_equal. apply: Lg_exten => //;move=> j js. have pd: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. rewrite /g''; bw. by rewrite OT_prop4 //; apply: order_type_exists. Qed. Lemma OT_prod_assoc1 r g r' g': worder r -> substrate r = domain g -> order_type_fam g -> worder r' -> substrate r' = domain g' -> worder_fam g' -> r = order_sum r' g' -> (forall i, inc i (domain g') -> finite_set (substrate (Vg g' i))) -> let order_prod_assoc_aux := fun l => OT_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in OT_prod r g = OT_prod r' (Lg (domain g') order_prod_assoc_aux). Proof. move=> wor sr alB wor' sr' alw oal alfs osa. rewrite /OT_prod. have oa': orsum_ax r' g'. by split;fprops; move => t ta; move: (proj1 (alw _ ta)). apply: order_type_unique. set g'' := (Lg (domain g) (fun z => order_type_of (Vg g z))). have oa: orprod_ax r g''. rewrite /g'';red; bw;split => //; hnf;bw; move=> i idg; bw. apply: (OT_prop3 (OT_prop2 (alB _ idg))). move: (orprod_assoc_iso oa oa' oal wor' alw) => /=. set aux' := fun l => order_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))). set f:= Lf _ _ _. move => oi1; move: (oi1) => [o1 o2 _ _]. apply: (@orderIT (order_prod r' (Lg (domain g') aux'))); first by exists f. apply: orprod_invariant2 =>//; bw; fprops. rewrite sr';move=> i isr; bw; rewrite /osa /OT_prod; bw. set s:= order_prod _ _. have -> : (aux' i = s). rewrite /aux' /s; apply: f_equal. apply: Lg_exten => //;move=> j js. have pd: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. rewrite /g''; bw. have os: order s. rewrite /s; apply: orprod_or; split;bw; first fprops. hnf; bw;move=> j js; bw. have jdg: inc (J j i) (domain g). rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. apply: (OT_prop3 (OT_prop2 (alB _ jdg))). by rewrite OT_prop4 //; apply: order_type_exists. Qed. Lemma OT_sum_assoc3 a b c: order_type a -> order_type b -> order_type c -> a +t (b +t c) = (a +t b) +t c. Proof. move => oa ob oc. have xoa: order (order_type_of a) by apply: OT_prop3; apply: OT_prop2. have xob: order (order_type_of b) by apply: OT_prop3; apply: OT_prop2. have xoc: order (order_type_of c) by apply: OT_prop3; apply: OT_prop2. rewrite/OT_sum2; apply: order_type_unique. have pa: order (order_sum2 (order_type_of b) (order_type_of c)). by apply: orsum2_or. have pb: order (order_sum2 (order_type_of a) (order_type_of b)). by apply: orsum2_or. rewrite OT_prop4 // OT_prop4 //. apply: (@orderIT (order_sum2 (order_type_of a) (order_sum2 (order_type_of b) (order_type_of c)))). apply: orsum_invariant4; [by apply: orderIR | by apply: OT_prop0 ]. apply: (@orderIT (order_sum2 (order_sum2 (order_type_of a) (order_type_of b))(order_type_of c))). apply: osum_assoc2; fprops. apply: orsum_invariant4; [ by apply: order_type_exists | by apply: orderIR]. Qed. Lemma OT_prod_assoc3 a b c: order_type a -> order_type b -> order_type c -> a *t (b *t c) = (a *t b) *t c. Proof. move => oa ob oc. have xoa: order (order_type_of a) by apply: OT_prop3; apply: OT_prop2. have xob: order (order_type_of b) by apply: OT_prop3; apply: OT_prop2. have xoc: order (order_type_of c) by apply: OT_prop3; apply: OT_prop2. rewrite/OT_prod2; apply: order_type_unique. have pa: order (order_prod2 (order_type_of b) (order_type_of c)). by apply: orprod2_or. have pb: order (order_prod2 (order_type_of a) (order_type_of b)). by apply: orprod2_or. rewrite OT_prop4 // OT_prop4 //. apply: (@orderIT (order_prod2 (order_type_of a) (order_prod2 (order_type_of b) (order_type_of c)))). apply: orprod_invariant4; [ by apply: orderIR |by apply: OT_prop0 ]. apply: (@orderIT (order_prod2 (order_prod2 (order_type_of a) (order_type_of b))(order_type_of c))). apply: oprod_assoc2; fprops. apply: orprod_invariant4; [ by apply: order_type_exists | by apply: orderIR]. Qed. Lemma OT_sum_distributive3 a b c: order_type a -> order_type b -> order_type c -> c *t (a +t b) = (c *t a) +t (c *t b). Proof. move => oa ob oc. rewrite /OT_sum2 /OT_prod2; apply: order_type_unique. have xoa: order (order_type_of a) by apply: OT_prop3; apply: OT_prop2. have xob: order (order_type_of b) by apply: OT_prop3; apply: OT_prop2. have xoc: order (order_type_of c) by apply: OT_prop3; apply: OT_prop2. have pa: order (order_prod2 (order_type_of c) (order_type_of a)). by apply: orprod2_or. have pb: order (order_prod2 (order_type_of c) (order_type_of b)). by apply: orprod2_or. have pc: order (order_sum2 (order_type_of a) (order_type_of b)). by apply: orsum2_or. rewrite OT_prop4 // OT_prop4 // OT_prop4 //. apply: (@orderIT (order_prod2 (order_type_of c) (order_sum2 (order_type_of a) (order_type_of b)))). apply: orprod_invariant4; [ by apply: orderIR | by apply: OT_prop0]. apply: (@orderIT (order_sum2 (order_prod2 (order_type_of c) (order_type_of a)) (order_prod2 (order_type_of c) (order_type_of b)))). apply: osum_distributive => //. by apply: orsum_invariant4;apply: order_type_exists. Qed. Lemma OT_sum_increasing2 r f g: order r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) -> (OT_sum r f) <=t (OT_sum r g). Proof. move=> wor sf sg alo. have Xa: orsum_ax r (Lg (domain f) (fun z : Set => order_type_of (Vg f z))). split => //;hnf; bw; move=> i isf; bw. move: (alo _ isf) => [pa pb _]. by apply: OT_prop3; apply: OT_prop2. have Xb: orsum_ax r (Lg (domain g) (fun z : Set => order_type_of (Vg g z))). split => //; hnf;bw; rewrite - sg sf. move=> i isf; bw;move: (alo _ isf) => [pa pb _]. by apply: OT_prop3; apply: OT_prop2. have pa:order (order_sum r (Lg (domain f) (fun z => order_type_of (Vg f z)))). by apply: orsum_or. have pb:order (order_sum r (Lg (domain g) (fun z => order_type_of (Vg g z)))). by apply: orsum_or. have pc: order_type (OT_sum r f) by apply: OT_prop1. have pd: order_type (OT_sum r g) by apply: OT_prop1. apply / OTorder_le_altP;split =>// ; apply: order_le_alt4. apply /(OTorder_le_compatP pa pb); apply:osum_increasing1 => //. bw; move=> x xdf; bw; last by rewrite - sg sf. move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2]. by move /(OTorder_le_compatP (OT_prop2 ot1) (OT_prop2 ot2)). Qed. Lemma OT_prod_increasing2 r f g: worder r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) -> (OT_prod r f) <=t (OT_prod r g). Proof. move=> wor sf sg alo. have Xa: orprod_ax r (Lg (domain f) (fun z : Set => order_type_of (Vg f z))). split => //;hnf ;bw; move=> i isf; bw. move: (alo _ isf) => [pa pb _]. by apply: OT_prop3; apply: OT_prop2. have Xb: orprod_ax r (Lg (domain g) (fun z : Set => order_type_of (Vg g z))). split => //; hnf;bw; rewrite - sg sf. move=> i isf; bw;move: (alo _ isf) => [pa pb _]. by apply: OT_prop3; apply: OT_prop2. have pa:order (order_prod r (Lg (domain f) (fun z => order_type_of (Vg f z)))). by apply: orprod_or. have pb:order (order_prod r (Lg (domain g) (fun z => order_type_of (Vg g z)))). by apply: orprod_or. have pc: order_type (OT_prod r f) by apply: OT_prop1. have pd: order_type (OT_prod r g) by apply: OT_prop1. apply /OTorder_le_altP;split => //; apply: order_le_alt4. apply /(OTorder_le_compatP pa pb). apply: oprod_increasing1 => //. bw; move=> x xdf; bw; last by rewrite - sg sf. move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2]. by move /(OTorder_le_compatP (OT_prop2 ot1)(OT_prop2 ot2)). Qed. Lemma OT_sum_increasing4 r f j: order r -> substrate r = domain f -> sub j (domain f) -> order_type_fam f -> (OT_sum (induced_order r j) (restr f j)) <=t (OT_sum r f). Proof. move => or sr sjf alo. have sjr: sub j (substrate r) by ue. have dr: (domain (restr f j)) = j by rewrite restr_d //. have Xa: orsum_ax r (Lg (domain f) (fun z => order_type_of (Vg f z))). split => //; hnf; bw;move=> i isf; bw;move: (alo _ isf) => iot. by apply: OT_prop3; apply: OT_prop2. have pa:order (order_sum r (Lg (domain f) (fun z => order_type_of (Vg f z)))). by apply: orsum_or. have pc: order_type (OT_sum r f) by apply: OT_prop1. have dj: j = domain (restr f j) by rewrite restr_d. move: (iorder_osr or sjr) => [pa' pb']. have p2: orsum_ax (induced_order r j) (Lg (domain (restr f j)) (fun z : Set => order_type_of (Vg (restr f j) z))). split;fprops;bw;aw; hnf; bw; move=> i idf; bw. move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot. by apply: OT_prop3; apply: OT_prop2. have pb: order (order_sum (induced_order r j) (Lg (domain (restr f j)) (fun z => order_type_of (Vg (restr f j) z)))). by apply: orsum_or. have pd: order_type (OT_sum (induced_order r j) (restr f j)). by apply: OT_prop1. apply /OTorder_le_altP; split => //; apply: order_le_alt4. apply /(OTorder_le_compatP pb pa). set g:= (Lg (domain f) (fun z : Set => order_type_of (Vg f z))). have fgg: fgraph g by rewrite /g; fprops. have sjdg: sub j (domain g) by rewrite /g; bw; ue. have ->: (Lg (domain (restr f j)) (fun z => order_type_of (Vg (restr f j) z))) = restr g j. by apply: fgraph_exten;fprops; bw;rewrite /g; move => k kj /= ;bw; apply: sjf. apply: osum_increasing3 => //. Qed. Lemma OT_prod_increasing4 r f j: worder r -> substrate r = domain f -> sub j (domain f) -> order_type_fam f -> (forall x, inc x ((domain f) -s j) -> substrate (Vg f x) <> emptyset) -> (OT_prod (induced_order r j) (restr f j)) <=t (OT_prod r f). Proof. move => or sr sjf alo alne . have sjr: sub j (substrate r) by ue. have dr: (domain (restr f j)) = j by rewrite restr_d //. have Xa: orprod_ax r (Lg (domain f) (fun z => order_type_of (Vg f z))). split => //; hnf;bw; move=> i isf; bw;move: (alo _ isf) => iot. by apply: OT_prop3; apply: OT_prop2. have pa:order (order_prod r (Lg (domain f) (fun z => order_type_of (Vg f z)))). by apply: orprod_or. have pc: order_type (OT_prod r f) by apply: OT_prop1. have dj: j = domain (restr f j) by rewrite restr_d. have odr: order r by move: or => [ok _]. have p2: orprod_ax (induced_order r j) (Lg (domain (restr f j)) (fun z : Set => order_type_of (Vg (restr f j) z))). have woi: worder (induced_order r j) by apply:induced_wor. split => //; bw; aw; hnf; bw=> i idf; bw. move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot. by apply: OT_prop3; apply: OT_prop2. have pb: order (order_prod (induced_order r j) (Lg (domain (restr f j)) (fun z => order_type_of (Vg (restr f j) z)))). by apply: orprod_or. have pd: order_type (OT_prod (induced_order r j) (restr f j)). by apply: OT_prop1. apply/OTorder_le_altP; split => //; apply: order_le_alt4. apply /(OTorder_le_compatP pb pa). set g:= (Lg (domain f) (fun z : Set => order_type_of (Vg f z))). have fgg: fgraph g by rewrite /g; fprops. have sjdg: sub j (domain g) by rewrite /g; bw; ue. have ->: (Lg (domain (restr f j)) (fun z=> order_type_of (Vg (restr f j) z))) = restr g j. by apply: fgraph_exten; fprops; bw;rewrite /g; move => k kj /= ;bw;apply: sjf. apply: oprod_increasing3 => //. move=> x; rewrite /g Lg_domain => xg. have xdf: inc x (domain f) by move: xg => /setC_P []. bw; move: (alne _ xg) => t; dneg bad. move: (order_type_exists (OT_prop2 (alo _ xdf))) => [h [_ _ [[[fh _] _] sh tgh] _]]. apply /set0_P => t' ts. empty_tac1 (Vf h t'); rewrite - tgh; Wtac. Qed. Lemma OT_prod_pr1 a b c: order_type a -> order_type b -> worder c -> b \Is c -> a *t b = OT_sum c (cst_graph (substrate c) a). Proof. move=> ota otb woc ibc. rewrite /OT_prod2 /OT_sum. have ora: order a by apply: OT_prop2. have orb: order b by apply: OT_prop2. move: (proj1 woc) => oc. apply: order_type_unique. have ->: domain (cst_graph (substrate c) a) = substrate c. rewrite /cst_graph; bw. apply: (@orderIT (order_prod2 a b)). by apply: orprod_invariant4; apply: OT_prop0. move: (order_prod_pr ora orb);set aux := order_sum _ _ ; move=> h. apply: (@orderIT aux) => //. move: ibc => [f isf]. rewrite /aux /cst_graph; apply: (orsum_invariant1(f:=f)); bw => //. move: isf => [_ _ [[[ff _] _] sf tf] _]. rewrite - sf; move=> i id. move: (Vf_target ff id); rewrite -tf=> vt. by bw ; apply: order_type_exists. Qed. Definition OT_opposite x := order_type_of (opp_order x). Lemma OT_opposite1 a b: a \Is b -> (opp_order a) \Is (opp_order b). Proof. move=> [f [o1 o2 bp isf]]. move: (opp_osr o1)(opp_osr o2) => [pa pb][pc pd]. exists f;split => //;fprops; rewrite ? pb ? pd //. move=> x y asf bsf. by split; move /opp_gleP /(isf _ _ bsf asf) /opp_gleP. Qed. Lemma OT_opposite2 x: order x -> opp_order (opp_order x) = x. Proof. move =>[pa _ _ _]; apply :(igraph_involutive pa). Qed. Lemma OT_opposite3 a: order a -> OT_opposite (order_type_of a) = OT_opposite a. Proof. move => oa. by apply: order_type_unique; apply:OT_opposite1; apply:OT_prop0. Qed. Lemma OT_double_opposite x: order_type x -> OT_opposite (OT_opposite x) = x. Proof. move=> otx; rewrite /OT_opposite. have ox : order x by apply: OT_prop2. have xp1: x= order_type_of x by move: otx => [y yo yp]; rewrite yp OT_prop4 //. rewrite {2} xp1; apply: order_type_unique. rewrite -{2} (OT_opposite2 ox);apply: OT_opposite1. apply: OT_prop0; apply: (proj1 (opp_osr ox)). Qed. Lemma OT_opposite_sum r f: order r -> substrate r = domain f -> order_type_fam f -> OT_opposite (OT_sum r f) = OT_sum (opp_order r) (Lg (substrate r) (fun z => OT_opposite (Vg f z))). Proof. move=> or sr alo. rewrite /OT_opposite /OT_sum Lg_domain; apply: order_type_unique. set s1 := order_sum _ _. have alor : forall x , inc x (domain f) -> order (Vg f x). move=> i idf; apply: (OT_prop2 (alo _ idf)). set s2:= order_sum r (Lg (domain f) (fun z => (Vg f z))). apply: (@orderIT (opp_order s2)). apply: OT_opposite1;apply: (@orderIT s1). apply: OT_prop0. apply: orsum_or; bw;split => //; hnf; bw => i idf; bw. apply: (OT_prop3 (alor _ idf)). rewrite /s1 /s2. apply: orsum_invariant2 ; bw; fprops. rewrite sr;move=> i isr; bw; apply: (OT_prop0 (alor _ isr)). set g := (Lg (domain f) (fun z => (opp_order (Vg f z)))). move: (opp_osr or) => [pa pb]. have ta: orsum_ax (opp_order r) g. rewrite /g;split => //;fprops;aw; bw;first by ue. hnf; bw;move=> i idf; bw; exact: (proj1 (opp_osr (alor _ idf))). have os2: order s2. by apply: orsum_or; split => //; hnf; bw; move=> i idf; bw; apply: alor. have tb:orsum_ax r (Lg (domain f) (fun z => Vg f z)). split => //; bw;aw;hnf;bw. move=> i idf; bw; move: (alor _ idf) => aux; fprops. have osg: order (order_sum (opp_order r) g) by apply: orsum_or. have ss:substrate (order_sum (opp_order r) g) = substrate s2. rewrite /s2 orsum_sr // orsum_sr //. rewrite /sum_of_substrates /fam_of_substrates /g; bw. apply: f_equal; apply: Lg_exten => // x xdf; bw. apply (proj2 (opp_osr (alor _ xdf))). apply: (@orderIT (order_sum (opp_order r) g)). move: ( identity_fb (substrate s2)) => hh. move: (opp_osr os2) => [oo3 sr2]. exists (identity (substrate s2)). split;fprops; first split;aw; fprops. hnf;aw;move => x y xsr ysr; rewrite !identity_V //. have qy:inc (Q y) (domain f). move: ysr; rewrite /s2 orsum_sr // => h. move: (du_index_pr1 h) => [h1 _]; move: h1; bw. have qx:inc (Q x) (domain f). move: xsr; rewrite /s2 orsum_sr // => h. move: (du_index_pr1 h) => [h1 _]; move: h1; bw. have sgs2: sum_of_substrates g = substrate s2. by move: ss; rewrite /s2 orsum_sr // orsum_sr //. have sgs3: (sum_of_substrates (Lg (domain f) (Vg f))) = substrate s2. rewrite /s2 orsum_sr //. split. move /opp_gleP => ha; apply /orsum_gleP; rewrite sgs2;split => //. move: ha => /orsum_gleP [pa' pb']; case => pc. by left; apply /opp_gltP. rewrite /order_sum_r;right; move: pc => []; bw; move => -> pc; split => //. by rewrite /g; bw; apply /opp_gleP. move /orsum_gleP => [_ _ h]; apply /opp_gleP; apply /orsum_gleP. rewrite sgs3;split => //; case: h; first by move /opp_gltP => h;left. move => [sq]; rewrite /g; bw;move /opp_gleP => h. right; bw;split => //; ue. apply: orsum_invariant2 => //; rewrite /g pb; bw. rewrite sr;move=> i isr; bw. move: (alor _ isr) => aux. have aux2: order (opp_order (Vg f i)) by apply: (proj1 (opp_osr (alor _ isr))). by rewrite OT_prop4 //; apply: order_type_exists. Qed. Require Import ssete2 ssetq2. (** The eta order of Cantor *) Definition Cantor_eta := order_type_of BQ_int01_ordering. Lemma Cantor_eta_prop2 r: eta_like r -> order_type_of r = Cantor_eta. Proof. move => ra. apply: order_type_unique; apply: (Cantor_eta_pr ra eta_likeQp_int01). Qed. Lemma Cantor_etaP r: order r -> (eta_like r <-> order_type_of r = Cantor_eta). Proof. move => or;split; first by apply:Cantor_eta_prop2. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. move => h;move: (OT_prop0 or) (OT_prop0 (proj1 pa)). rewrite -/Cantor_eta h => sa sb; move: (orderIT (orderIS sa) sb). move => [f [_ _ fp sincf]] {h sa sb}. have csr: cardinal (substrate r) = aleph0. by rewrite - pe; apply /card_eqP; exists f. have ccsr:= (aleph0_countable csr). move: fp => [bf sf tf]; move: (proj1 (proj1 bf)) => ff. split => //; split => //. + split => // x y; rewrite - sf => xsr ysr. move: (Vf_target ff xsr) (Vf_target ff ysr); rewrite tf => xa ya. case: (proj2 pa _ _ xa ya) => h. by left; move/(sincf x y xsr ysr): h. by right; move/(sincf y x ysr xsr): h. + move => x; rewrite - sf => xsr; move: (Vf_target ff xsr); rewrite tf => xa. move:(pb (Vf f x) xa) => [z ylx]. have: inc z (substrate BQ_int01_ordering) by order_tac. rewrite - tf => zt; move: (bij_surj bf zt) => [y ysf yv]; exists y. move:ylx; rewrite - yv; move => [ra rb]; split; last by dneg hh; rewrite hh. by apply /(sincf y x ysf xsr). + move => x; rewrite - sf => xsr; move: (Vf_target ff xsr); rewrite tf => xa. move:(pc (Vf f x) xa) => [z ylx]. have: inc z (substrate BQ_int01_ordering) by order_tac. rewrite - tf => zt; move: (bij_surj bf zt) => [y ysf yv]; exists y. move:ylx; rewrite - yv; move => [ra rb]; split; last by dneg hh; rewrite hh. by apply /(sincf x y xsr ysf). + move => x y [lxy nxy]. have: inc x (substrate r) by order_tac. have: inc y (substrate r) by order_tac. rewrite - sf => ysr xsr. move/(sincf x y xsr ysr): lxy => le1. have: glt BQ_int01_ordering (Vf f x) (Vf f y). by split => //; move /(proj2 (proj1 bf) _ _ xsr ysr). move /pd => [u [[ua ub] [uc ud]]]. have: inc u (substrate BQ_int01_ordering) by order_tac. rewrite - tf => zt; move: (bij_surj bf zt) => [z zsr zv]; exists z. rewrite - zv in ua ub uc ud. split; split. + by apply /(sincf _ _ xsr zsr). + clear ud;dneg hh; ue. + by apply /(sincf _ _ zsr ysr). + dneg hh; ue. Qed. Lemma Cantor_eta_pr1: order_type_of Nat_order <> Cantor_eta. Proof. move:Nat_order_wor => [[or _] sr]. move/(Cantor_etaP or) => [[_ _ h _ _] _]. by rewrite sr in h; move:(h _ NS0) => [y [/Nat_order_leP[_ _ /cle0 h3]]]. Qed. Definition singleton_order := singleton (J emptyset emptyset). Definition singleton_OT := order_type_of singleton_order. Notation "\1t" := singleton_OT. Lemma singleton_order_or: order singleton_order. Proof. exact: (proj1 (proj1 (set1_wor emptyset))). Qed. Lemma OT_1_or : order \1t. Proof. exact: (OT_prop3 singleton_order_or). Qed. Lemma OT_eta_1 : order Cantor_eta. Proof. apply:(OT_prop3 (proj1 BQ_int01_or_osr)). Qed. Lemma singleton_OT_pr: exists x, \1t = singleton (J x x). Proof. move: (set1_wor emptyset) => [[or _] sr]. move: (OT_prop0 or) => [f []]. rewrite sr -/singleton_order -/ singleton_OT => o1 _ fp fc. apply: set1_order_is1 => //; apply/ set_of_card_oneP. by rewrite -(cardinal_set1 emptyset); apply /card_eqP; exists f. Qed. Lemma OT_cardinal_1: cardinal (substrate singleton_order) = \1c. Proof. by rewrite (proj2 (set1_wor emptyset)) cardinal_set1. Qed. Lemma Cantor_eta_pr2: Cantor_eta +t \1t <> Cantor_eta. Proof. move:BQ_int01_or_osr => [or1 sr1]. move: (set1_wor emptyset) => [[or2 _] sr2]. move: (orsum2_osr or1 or2) => [pc pd]. rewrite (OT_sum2_pr2 or1 or2); move /(Cantor_etaP pc). rewrite -/singleton_order. move => [[qa qb _ qd _] _]. move: pd; rewrite sr2 sr1; set E := canonical_du2 _ _ => pd. have xE: inc (J emptyset C1) E by apply:candu2_prb; fprops. rewrite pd in qd; move: (qd _ xE) => [y [/orsum2_gleP [_ yE lxy]] nexy]. move /candu2P: yE => [ya yb]. move: lxy; aw; case; move => []; fprops => sa sb;case: yb; move => [sc sd] //. move/set1_P => /pr2_def h; case nexy; symmetry;apply: pair_exten; fprops; aw. Qed. Lemma orsum_total r g: orsum_ax r g -> total_order r -> (forall i, inc i (domain g) -> total_order (Vg g i)) -> total_order (order_sum r g). Proof. move=> oa [_ tor] alt; rewrite /total_order. move: (oa) => [or sr alo]; bw. rewrite sr in tor. split =>//; first by fprops. move=> x y xsr ysr; move: (du_index_pr1 xsr) (du_index_pr1 ysr). move=> [Qx Px px][Qy Py py]. case: (equal_or_not (Q x) (Q y)). move =>h; move: (alt _ Qx) => [lor ltor]; rewrite -h in Py. case: (ltor _ _ Px Py) => h1;aw ; [left | right]; apply /orsum_gleP;split => //; right; split => //; ue. move=> nQ; case: (tor _ _ Qx Qy) => h; [left | right]; apply /orsum_gleP;split => //; left;split; fprops. Qed. Lemma orsum2_totalorder r r': total_order r -> total_order r' -> total_order (order_sum2 r r'). Proof. move: cdo_wor => [ha hb]. have hc:= (worder_total ha). have hd := proj1 ha. move => pa pb; move:(pa)(pb) => [oa _][ob _]; apply: orsum_total => //. hnf; split => //; [ bw | hnf; bw => x xi; try_lvariant xi]. hnf;bw => x xi; try_lvariant xi. Qed. Lemma Cantor_eta_pr3: \1t +t Cantor_eta <> Cantor_eta. Proof. move:BQ_int01_or_osr => [or1 sr1]. move: (set1_wor emptyset) => [[or2 _] sr2]. move: (orsum2_osr or2 or1) => [pc pd]. rewrite (OT_sum2_pr2 or2 or1); move /(Cantor_etaP pc). rewrite -/singleton_order. move => [[_ _ qd _ _] _]. move: pd; rewrite sr2 sr1; set E := canonical_du2 _ _ => pd. have xE: inc (J emptyset C0) E by apply:candu2_pra; fprops. rewrite pd in qd; move: (qd _ xE) => [y [/orsum2_gleP [yE _ lxy]] nexy]. move /candu2P: yE => [ya yb]. move: lxy; aw; case; move => []; fprops => sa _ ;case: yb; move => [sc sd] //. move/set1_P => /pr1_def h; case nexy;apply: pair_exten; fprops; aw. by case: C0_ne_C1; rewrite - sa - sd. Qed. Lemma Cantor_eta_pr4: Cantor_eta +t Cantor_eta = Cantor_eta. Proof. move:BQ_int01_or_osr => [or1 sr1]. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. move: (orsum2_osr or1 or1) => [pf pg]. set r := BQ_int01_ordering. set E := substrate (order_sum2 r r). move: C1_ne_C0 => nT. move: C0_ne_C1 => nT1. have cE: cardinal E = aleph0. rewrite /E pg cardinal_du2 pe; apply:aleph0_pr2. have ccE:= aleph0_countable cE. rewrite (OT_sum2_pr2 or1 or1); apply /(Cantor_etaP pf); split => //. split => //. + by apply: orsum2_totalorder. + rewrite pg; move => x xsr; move:(xsr) => /candu2P [px] [] [p1x p2x]. move:(pb _ p1x) => [y [yp yne]]; exists (J y C0); split; last first. by rewrite - px => /pr1_def. apply/orsum2_gleP; split => //; last by constructor 1; aw. apply/candu2P; split; fprops; aw;left; split => //;order_tac. move:(pb _ p1x) => [y [yp yne]]; exists (J y C1); split; last first. by rewrite - px => /pr1_def. apply/orsum2_gleP; split => //. apply/candu2P; split; fprops; aw; right; split => //;order_tac. constructor 2; aw; rewrite p2x;split => //. + rewrite pg; move => x xsr; move:(xsr) => /candu2P [px] [] [p1x p2x]. move:(pc _ p1x) => [y [yp yne]]; exists (J y C0); split; last first. by rewrite - px => /pr1_def. apply/orsum2_gleP; split => //; last by constructor 1; aw. apply/candu2P; split; fprops; aw;left; split => //;order_tac. move:(pc _ p1x) => [y [yp yne]]; exists (J y C1); split; last first. by rewrite - px => /pr1_def. apply/orsum2_gleP; split => //. apply/candu2P; split; fprops; aw; right; split => //;order_tac. constructor 2; aw; rewrite p2x;split => //. + move => x y [ /orsum2_gleP [xsr ysr lexy] nexy]. move/candu2P:(xsr)=> [px xsr']; move /candu2P : (ysr) =>[py ysr']. case: lexy. move => [x0 y0 lexy]. have: glt r (P x) (P y). by split => // spy; case: nexy; apply: pair_exten => //; rewrite x0 y0. move => /pd [z [[za zb] [zc zd]]]; exists (J z C0); split; split. - apply/orsum2_gleP; split => //; first by apply: candu2_pra; order_tac. by aw; constructor 1. - by rewrite - px => /pr1_def. - apply/orsum2_gleP; split => //; first by apply: candu2_pra; order_tac. by aw; constructor 1. - by rewrite - py => /pr1_def. move => [x0 y0 lexy]. have x1 : Q x = C1 by case: xsr' => [][]. have y1 : Q y = C1 by case: ysr' => [][]. have: glt r (P x) (P y). by split => // spy; case: nexy; apply: pair_exten => //; rewrite x1 y1. move => /pd [z [[za zb] [zc zd]]]; exists (J z C1); split; split. - apply/orsum2_gleP; split => //; first by apply: candu2_prb; order_tac. by aw; constructor 2. - by rewrite - px => /pr1_def. - apply/orsum2_gleP; split => //; first by apply: candu2_prb; order_tac. by aw; constructor 2. - by rewrite - py => /pr1_def. move => [x0 y0]. have y1 : Q y = C1 by case: ysr' => [][]. have xsr2 : inc (P x) (substrate r) by case: xsr' => [][]. have ysr2 : inc (P y) (substrate r) by case: ysr' => [][]. move: (pc _ xsr2) => [z [za zb]]; exists (J z C0); split. split; last by rewrite -px => /pr1_def. apply /orsum2_gleP; split => //; first by apply: candu2_pra; order_tac. constructor 1; aw; split => //. rewrite - py y1;apply: orsum2_gle_spec => //; order_tac. Qed. Lemma Cantor_eta_pr5: Cantor_eta +t \1t +t Cantor_eta = Cantor_eta. Proof. move:BQ_int01_or_osr => [or1 sr1]. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. set r := BQ_int01_ordering. move: singleton_order_or => or2. move: (orsum2_osr or1 or2) => [or3 sr3]. move: (orsum2_osr or3 or1) => [or4]. set E := substrate _ => sr4. have cE: cardinal E = aleph0. rewrite sr4 cardinal_du2 sr3 cardinal_du2 pe OT_cardinal_1 aleph0_plus1. apply:aleph0_pr2. rewrite {1} /OT_sum2 (OT_sum2_pr2 or1 or2). rewrite - /(OT_sum2 _ _) (OT_sum2_pr2 or3 or1). move: (set1_wor emptyset) => [wor2 sr2]. move: sr4; rewrite sr3; rewrite sr2;set T := (substrate r) => sr4. set T1 := (substrate singleton_order). have oneT: inc \2hq T. have ra:= QSh2; move/ qlt0xP:QpsSh2 => hp. have rc: \2hq nT. move: C1_ne_C0 => nT1. apply /(Cantor_etaP or4); split => //; split. + apply: orsum2_totalorder => //; apply: orsum2_totalorder => //. exact: (worder_total wor2). + exact: (aleph0_countable cE). + rewrite -/E sr4; move => x xsr. move:(xsr); rewrite - sr2 - sr3 => xsr1. move:(xsr) => /candu2P [px []]; case => [p1x p2x]. have aux2: inc (P x) (canonical_du2 T T1) by rewrite /T1 sr2. move/candu2P: (p1x) => [ppx []]; case => [p3x p4x]. move: (pb _ p3x) => [y [lxy nxy]]; exists (J (J y C0) C0). split; last by rewrite - px - ppx => /pr1_def /pr1_def. have aux: inc (J y C0) (canonical_du2 T T1). apply: candu2_pra; rewrite /T;order_tac. apply/orsum2_gleP; split. - by apply: candu2_pra; rewrite sr3. - exact. - constructor 1; split => //; aw; apply/orsum2_gleP; split => //. constructor 1; split => //; aw. exists (J (J \2hq C0) C0); split; last first. by rewrite - px - ppx p4x => /pr1_def /pr2_def. have aux: inc (J \2hq C0) (canonical_du2 T T1) by apply: candu2_pra. apply/orsum2_gleP; split. - by apply: candu2_pra; rewrite sr3. - exact. - constructor 1; split => //; aw; apply/orsum2_gleP; split => //. by rewrite p4x;constructor 3; aw. exists (J (J emptyset C1) C0). rewrite -px p2x; apply: orsum2_gle_spec => //. rewrite sr3 sr2; apply:candu2_prb;fprops. + rewrite -/E sr4; move => x xsr. move:(xsr); rewrite - sr2 - sr3 => xsr1. move:(xsr) => /candu2P [px []]; case => [p1x p2x]. exists (J \2hq C1); rewrite - px p2x; apply: orsum2_gle_spec => //. by rewrite sr3 sr2. move: (pc _ p1x) => [y [lxy nxy]]; exists (J y C1); split; last first. by rewrite - px => /pr1_def. apply/orsum2_gleP; split => //; first by apply: candu2_prb; order_tac. constructor 2; aw; rewrite p2x; split => //. + move => x y [/orsum2_gleP [xsr ysr lexy] nexy]. move /candu2P: (ysr) => [py ysr0]. move /candu2P: (xsr) => [px xsr0]. case: lexy. - move => [x0 y0 /orsum2_gleP [xsr1 ysr1]]. move/candu2P:(xsr1) => [ppx qpx]. move/candu2P:(ysr1) => [ppy qpy]. case. * move => [px0 py0 le2]. have:glt r (P (P x)) (P (P y)). by split =>// h; case:nexy;rewrite - px - py - ppx -ppy h px0 py0 x0 y0. move/pd => [z [[za zb] [zc zd]]]. have aux0: inc (J z C0) (canonical_du2 T (substrate singleton_order)). apply: candu2_pra; rewrite /T; order_tac. have aux: inc (J (J z C0) C0) (canonical_du2 (substrate (order_sum2 r singleton_order)) T). by apply: candu2_pra; rewrite sr3. exists (J (J z C0) C0); split; split. + apply/orsum2_gleP;split => //; constructor 1; aw; split => //. by apply/orsum2_gleP;split => //; constructor 1; aw. + by rewrite - px - ppx => /pr1_def /pr1_def. + apply/orsum2_gleP;split => //; constructor 1; aw; split => //. by apply/orsum2_gleP;split => //; constructor 1; aw. + by rewrite - py - ppy => /pr1_def /pr1_def. * move => [px0 py0 le2]. move:qpy; case; move => [ha hb]; first by case: py0. move:qpx; case; move => [hc hd]; first by case: py0. case: nexy; apply: pair_exten => //; last by rewrite x0 y0. apply: pair_exten => //; last by rewrite hb hd. by move: ha hc; rewrite sr2 => /set1_P -> /set1_P ->. * move => [px0 py1]; case: qpy; move => [yp1 yp2]; first by case: py1. case: qpx; move => [xp1 xp2]; last by case:C0_ne_C1; rewrite -px0 - xp2. move: (pc _ xp1) => [z [za zb]]. have aux0: inc (J z C0) (canonical_du2 T (substrate singleton_order)). apply: candu2_pra; rewrite /T; order_tac. have aux: inc (J (J z C0) C0) (canonical_du2 (substrate (order_sum2 r singleton_order)) T). by apply: candu2_pra; rewrite sr3. exists (J (J z C0) C0); split; split. + apply/(orsum2_gleP); split => //; constructor 1; aw; split => //. apply/(orsum2_gleP); split => //;aw; constructor 1; split => //. + by rewrite - px - ppx => /pr1_def /pr1_def. + apply/(orsum2_gleP); split => //; constructor 1; aw; split => //. by apply/(orsum2_gleP); split => //;aw; constructor 3. + by rewrite - py - ppy => /pr1_def /pr2_def /nesym. - move => [x1 y1 le1]. case: ysr0;move => [_ y0]; first by case y1. case: xsr0;move => [_ x0]; first by case x1. have: glt r (P x) (P y). by split => // exy; case: nexy; apply:pair_exten => //; rewrite x0 y0. move /pd => [z [[za zb] [zc zd]]]; exists (J z C1); split; split. * apply/orsum2_gleP; split => //; first by apply:candu2_prb; order_tac. by constructor 2; aw. * by rewrite - px => /pr1_def. * apply/orsum2_gleP; split => //; first by apply:candu2_prb; order_tac. by constructor 2; aw. + by rewrite - py => /pr1_def. - move => [x0 y1]. case: ysr0 => [] [sa y0]; first by case: y1. case: xsr0=> [] [sb x1];last by case: nT; rewrite - x0 - x1. rewrite - px x0. move:(pb _ sa) => [z [za zb]]. have zr: inc z (substrate r) by order_tac. exists (J z C1); split; first by apply: orsum2_gle_spec. split; last by rewrite - py => /pr1_def. apply/orsum2_gleP; split => //; first by apply: candu2_prb. constructor 2; aw; split => //. Qed. Lemma Cantor_eta_pr6: Cantor_eta *t Cantor_eta = Cantor_eta. Proof. move:BQ_int01_or_osr => [or1 sr1]. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. set r := BQ_int01_ordering. have H:= (orprod2_gleP or1 or1). move: (orprod2_osr or1 or1) => [pf pg]. set E := substrate (order_prod2 r r). set T := (substrate r). have cE: cardinal E = aleph0. have eq : T *c T = cardinal (product2 T T) by []. by rewrite /E pg -/T - eq - cprod2cr - cprod2cl pe aleph0_pr3. have ccE:= aleph0_countable cE. rewrite (OT_prod2_pr2 or1 or1); apply /(Cantor_etaP pf); split => //. split => //. + by apply: orprod2_totalorder. + rewrite pg; move => x xsr;move:(xsr) => /setX2_P [fgx dx x0 x1]. move:(pb _ x0) => [y yp]; exists (variantLc y (Vg x C1)); split. apply /H; split => //; last by right; bw. apply /setX2_P; split => //; fprops; bw; order_tac. move => hg; case: (proj2 yp); rewrite - hg; bw. + rewrite pg; move => x xsr;move:(xsr) => /setX2_P [fgx dx x0 x1]. move:(pc _ x0) => [y yp]; exists (variantLc y (Vg x C1)); split. apply /H; split => //; last by right; bw. apply /setX2_P; split => //; fprops; bw; order_tac. move => hg; case: (proj2 yp);rewrite hg; bw. + move => x y [/(orprod2_gleP or1 or1) [xsr ysr lxy] nxy]. move:(xsr) => /setX2_P [fgx dx x0 x1]. move:(ysr) => /setX2_P [fgy dy y0 y1]. case lxy. move => [sc0 lec1]. have: glt r (Vg x C1) (Vg y C1). split => //; dneg h1; apply: fgraph_exten => //; first by rewrite dx. rewrite dx;move => u udx; try_lvariant udx. move /pd => [z [[za zb][za' zb']]]; set z1 := (variantLc (Vg x C0) z). have zz:inc z1 (product2 T T). apply /setX2_P; rewrite /z1 /T;split => //; fprops; bw;order_tac. have zc: Vg z1 C1 = z by rewrite /z1; bw. have zd: Vg z1 C0 = Vg x C0 by rewrite /z1; bw. exists z1; split; split. + by apply /H; split => //; left; rewrite zc zd. + by move => h;case: zb; rewrite - zc h. + by apply /H; split => //; left; rewrite zc zd. + by move => h;case: zb'; rewrite - zc h. move/pd => [z [za zb]]; set z1 := (variantLc z (Vg x C1)). have zz:inc z1 (product2 T T). apply /setX2_P; rewrite /z1 /T;split => //; fprops; bw; order_tac. have zc: Vg z1 C0 = z by rewrite /z1; bw. exists z1; split; split. + by apply /H; split => //; right; rewrite zc. + by move => h;case: (proj2 za); rewrite - zc h. + by apply /H; split => //; right; rewrite zc. + by move => h;case: (proj2 zb); rewrite - zc h. Qed. Lemma Cantor_eta_pr7: OT_opposite Cantor_eta = Cantor_eta. Proof. move:BQ_int01_or_osr => [or1 sr1]. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. set r := BQ_int01_ordering. move: (opp_osr (proj1 pa)) => [sa sb]. have cE: cardinal (substrate (opp_order r)) = aleph0 by ue. have ccE:= aleph0_countable cE. rewrite (OT_opposite3 (proj1 pa)); apply /(Cantor_etaP sa); split => //. split => //. + by apply: total_order_opposite. + rewrite sb => x /pc [y lxy]; exists y; by apply/opp_gltP. + rewrite sb => x /pb [y lxy]; exists y; by apply/opp_gltP. + by move => x y /opp_gltP /pd [z [za zb]]; exists z; split; apply/opp_gltP. Qed. Notation "x <=q y" := (gle Qplus_or x y) (at level 60). Notation "x inc x Qplus /\ inc y Qplus. Proof. move => h; rewrite - Qplus_or_sr; split; order_tac. Qed. Lemma Qplus_cc x y: inc x Qplus1 -> inc y Qplus1 -> (class Qplus_eq x = class Qplus_eq y <-> Qplus_eq_r x y). Proof. move => pa pb. have ha: inc x (substrate Qplus_eq) by rewrite Qplus_eq_sr. have hb: inc y (substrate Qplus_eq) by rewrite Qplus_eq_sr. split => h. move/(related_equiv_P Qplus_equiv): (And3 ha hb h). by move/graph_on_P1 =>[]. have: related Qplus_eq x y by apply/graph_on_P1. by move/(related_equiv_P Qplus_equiv) => []. Qed. Lemma Qplus_cc1 a b c d: inc a Nat -> inc b Nstar -> inc c Nat -> inc d Nstar -> (class Qplus_eq (J a b) = class Qplus_eq (J c d) <-> a *c d = c *c b). Proof. move => pa pb pc pd. have ra: inc (J a b) Qplus1 by apply: setXp_i. have rb: inc (J c d) Qplus1 by apply: setXp_i. move:(Qplus_cc ra rb); rewrite /Qplus_eq_r; aw. Qed. Lemma NsS1 : inc \1c Nstar. Proof. apply/setC1_P; split; [apply: NS1 | fprops]. Qed. Lemma Qplus_inc3 x: inc x Qplus -> (inc (rep x) x /\ inc (rep x) Qplus1). Proof. move => h; move:(Qplus_inc1 h) => [ha hb]; split => //. exact: (setQ_repi Qplus_equiv h). Qed. Lemma Qplus_stable1 a b x: inc a Nat -> inc b Nats -> inc x Nats -> related Qplus_eq (J a b) (J (a *c x) (b *c x)). Proof. move => pa pb /setC1_P[pc pd]; apply/graph_on_P1; split => //. + by apply: setXp_i. + apply: setXp_i;first by apply:NS_prod. move/setC1_P: pb => [pc' pd']; apply/setC1_P; split;first by apply:NS_prod. by apply: cprod2_nz. by hnf; aw; rewrite (cprodC b) cprodA. Qed. Lemma Qplus_stable2 a b x: inc a Nat -> inc b Nats -> inc x Nats -> inc (J (a *c x) (b *c x)) (class Qplus_eq (J a b)). Proof. move => pa pb pc; move:(Qplus_stable1 pa pb pc) => pd. by apply /(class_P Qplus_equiv). Qed. Lemma Qplus_class_stable3 z y x: inc z Qplus -> inc y z -> inc x Nats -> inc (J ((P y) *c x) ((Q y) *c x)) z. Proof. move => pa pb pc. move: (inc_in_setQ_sr Qplus_equiv pb pa). rewrite Qplus_eq_sr => /setX_P [qa qb qc]. rewrite(is_class_pr Qplus_equiv pb pa) - {3} qa. by apply: Qplus_stable2. Qed. Definition Nat_to_Qplus n := class Qplus_eq (J n \1c). Definition Qplus_0 := Nat_to_Qplus \0c. Definition Qplus_1 := Nat_to_Qplus \1c. Notation "\0q" := Qplus_0. Notation "\1q" := Qplus_1. Lemma Nat_to_Qplus_aux n: natp n -> inc (J n \1c) Qplus1. Proof. move => h;apply:setXp_i => //; apply: NsS1. Qed. Lemma Nat_to_Qplus_Q n: natp n -> inc (Nat_to_Qplus n) Qplus. Proof. move=> /Nat_to_Qplus_aux Nn. by apply: inc_class_setQ; rewrite Qplus_eq_sr. Qed. Lemma Nat_to_Qplus_inj n m: natp n -> natp m -> (Nat_to_Qplus n) = (Nat_to_Qplus m) -> n = m. Proof. move => pa pb. move:(Nat_to_Qplus_aux pa)(Nat_to_Qplus_aux pb)=> pa' pb' pc'. by move/(Qplus_cc pa' pb'):pc'; rewrite /Qplus_eq_r; aw; apply:CS_nat. Qed. Lemma Nat_to_Qplus_le n m: natp n -> natp m -> n <=c m -> (Nat_to_Qplus n) <=q (Nat_to_Qplus m). Proof. move => pa pb pc. apply / (Qplus_or_gle1P (Nat_to_Qplus_aux pa) (Nat_to_Qplus_aux pb)). by hnf; aw; apply:CS_nat. Qed. Lemma Nat_to_Qplus_lt n m: natp n -> natp m -> n (Nat_to_Qplus n) pa pb [pc pd]; split. by apply:Nat_to_Qplus_le. by move => pe; case pd; apply:Nat_to_Qplus_inj. Qed. Lemma Qplus_0_pr: \0q = singleton \0c \times Nstar. Proof. move: Qplus_equiv Qplus_eq_sr => Ha sr. set_extens z. move =>/(class_P Ha) /graph_on_P1 [_ /setX_P [qa /CS_nat qb qc]]. rewrite /Qplus_eq_r; aw; rewrite cprodC cprod0r => ->. rewrite - {1} qa; apply: setXp_i; fprops. move => /setX_P [sa /set1_P zb zc]. apply/(class_P Ha) /graph_on_P1; split. + apply: Nat_to_Qplus_aux => //; apply: NS0. + apply/setX_P; split => //; rewrite zb; apply: NS0. rewrite /Qplus_eq_r zb; aw; [ by rewrite cprodC cprod0r |fprops ]. Qed. Lemma Qplus_0_least x: inc x Qplus -> \0q <=q x. Proof. move => h. move:(Qplus_inc1 h) => [sa ->]. apply/(Qplus_or_gle1P (Nat_to_Qplus_aux NS0) sa). rewrite /Qplus1_le_r pr1_pair pr2_pair cprodC cprod0r. by apply: czero_least; fprops. Qed. Definition Qplus_star := Qplus -s1 \0q. Lemma Qplus_0_least1 x: (\0q inc x Qplus_star. Proof. split. move => [pa pb]; apply/setC1_P;split; last by apply: nesym. exact(proj2 (Qplus_or_sr_bis pa)). move /setC1_P=> [pa pb]; split; last by apply: nesym. by apply:Qplus_0_least. Qed. Lemma Qplus_1_pr: \1q = diagonal Nstar. Proof. move: Qplus_equiv Qplus_eq_sr => Ha sr. set_extens z. move =>/(class_P Ha) /graph_on_P1 [_ /setX_P [qa /CS_nat qb qc]]. rewrite /Qplus_eq_r; aw. move => h; apply /diagonal_i_P; split => //; ue. by move/setC1_P: qc => [/CS_nat h _]. move/diagonal_i_P => [pa pb pc]. move:(pb); rewrite pc => pd. move /setC1_P: (pb) => [np _]; move:(CS_nat np) => cp. apply/(class_P Ha); apply/graph_on_P1;split. + apply: (Nat_to_Qplus_aux NS1). + by apply/setX_P. + by rewrite /Qplus_eq_r; aw; [by symmetry | by ue]. Qed. Lemma Qplus_le1_aux a b: inc a Nat -> inc b Nstar -> a <=c b -> (class Qplus_eq (J a b)) <=q \1q. Proof. move => ha hb hc; move:(hc) => [ca cb _]. have pa: inc (J a b) Qplus1 by apply:setXp_i. have pb:= Nat_to_Qplus_aux NS1. apply/(Qplus_or_gle1P pa pb); rewrite /Qplus1_le_r; aw. Qed. Lemma Qplus_le1 x: (x <=q \1q) <-> (inc x Qplus /\ (P (rep x) <=c (Q (rep x)))). Proof. split. move => h. have xq:=proj1 ( Qplus_or_sr_bis h). move:(Qplus_inc3 (Nat_to_Qplus_Q NS1)) => []; rewrite -/Qplus_1 => ha hb. move: ha;rewrite {2} Qplus_1_pr; move /diagonal_i_P => [_ hc hd]. split => //. move: (Qplus_inc3 xq) =>[_ /setX_P [_ sa /setC1_P [sb _]]]. move: (Qplus_or_gle2 h); rewrite /Qplus1_le_r - hd cprodC => he. move/setC1_P: hc => [pa pb]. apply:(cprod_le2l pa sa sb pb he). move => [pa pb]; move:(pb) => [ca cb _]. move: (Qplus_inc1 pa) => [pc pd]; rewrite pd. apply/(Qplus_or_gle1P pc (Nat_to_Qplus_aux NS1)); hnf; aw. Qed. Lemma Qplus_lt1 x: (x (inc x Qplus /\ (P (rep x) []; rewrite -/Qplus_1 => ha hb. move: ha;rewrite {2} Qplus_1_pr; move /diagonal_i_P => [_ hc hd]. split. move => [/Qplus_le1 [qa qb] qc]; split => //; split => // h; case: qc. move:(Qplus_inc1 qa) => [sa sb]; rewrite sb. move: (Qplus_inc3 qa) => [_ /setX_P [sc sd se]]. apply: (class_eq2 Qplus_equiv); rewrite -/(Nat_to_Qplus _) -/ Qplus_1. rewrite Qplus_1_pr; apply/diagonal_i_P; split => //; ue. move => [pa [pb pc]]; split; first by apply/ Qplus_le1. by move => ne; case pc; rewrite ne. Qed. Definition Qplus_half x := class Qplus_eq (J (P (rep x)) ((Q (rep x)) *c \2c)). Definition Qplus_double x := class Qplus_eq (J (P (rep x) *c \2c) (Q (rep x))). Definition Qplus_middle x y (a:= (P (rep x))) (b:= (Q (rep x))) (c:= (P (rep y))) (d:= (Q (rep y))) := class Qplus_eq (J (a *c d +c b *c c) (b *c d *c \2c)). Lemma Qplus_halfp x (y := Qplus_half x) : inc x Qplus_star -> inc y Qplus_star /\ y /setC1_P [xq xnz]. move:(Qplus_inc1 xq) => [sa sb]. move/setX_P: (sa) => [pa pb /setC1_P[pc pd]]. have rx: inc (Q (rep x) *c \2c) Nstar. apply/setC1_P;split; first by apply:NS_prod;fprops. apply: cprod2_nz => //; apply: card2_nz. have xi: inc (J (P (rep x)) (Q (rep x) *c \2c)) Qplus1 by apply: setXp_i. have ra: gle Qplus_or y x. rewrite sb;apply /(Qplus_or_gle1P xi sa);rewrite /Qplus1_le_r; aw. rewrite cprodA;apply:cprod_M1le; fprops. have pnz: P (rep x) <> \0c. move => k;case:xnz; rewrite sb; apply/(Qplus_cc sa (Nat_to_Qplus_aux NS0)). rewrite /Qplus_eq_r k; aw;[by rewrite cprodC cprod0r| fprops ]. have ynz: y <> Qplus_0. rewrite /y /Qplus_half /Qplus_0 / Nat_to_Qplus. move /(Qplus_cc1 pb rx NS0 NsS1). by rewrite (cprod1r (CS_nat pb)) cprodC cprod0r. split; first by apply/setC1_P; split => //; exact (proj1 (Qplus_or_sr_bis ra)). split => //; rewrite sb. move => /(Qplus_cc xi sa); rewrite /Qplus_eq_r; aw; rewrite cprodA => H. move: (cprod2_nz pnz pd) => h. move: (cprod_eq2l (NS_prod pb pc) NS1 NS2 h). rewrite cprod1r; fprops. Qed. Lemma Qplus_doublep x (y := (Qplus_double x)): inc x Qplus_star -> inc y Qplus_star /\ x h; suff: glt Qplus_or x y. move => h'; split => //. move/Qplus_0_least1:h => [la _]; apply/Qplus_0_least1. move: (proj1 Qplus_or_tor) => or;order_tac. move: h => /setC1_P [xq xnz]. move:(Qplus_inc1 xq) => [sa sb]. move/setX_P: (sa) => [pa pb pc1]; move/setC1_P: (pc1) => [pc pd]. have xi: inc(J (P (rep x) *c \2c) (Q (rep x))) Qplus1. by apply: setXp_i => //; apply:NS_prod;fprops. rewrite{1} sb;split. apply /(Qplus_or_gle1P sa xi);rewrite /Qplus1_le_r; aw. rewrite (cprodC _ \2c) - cprodA (cprodC \2c);apply:cprod_M1le; fprops. move => /(Qplus_cc sa xi); rewrite /Qplus_eq_r; aw. rewrite (cprodC _ \2c) - cprodA (cprodC \2c) => H. case (equal_or_not (P (rep x)) \0c) => h1. case:xnz; rewrite sb; apply/(Qplus_cc sa (Nat_to_Qplus_aux NS0)). rewrite /Qplus_eq_r h1; aw;[by rewrite cprodC cprod0r| fprops ]. move: (cprod2_nz h1 pd) => h. move: (cprod_eq2l (NS_prod pb pc) NS1 NS2 h). rewrite cprod1r; fprops. Qed. Lemma Qplus_middlep x y (z := Qplus_middle x y): x [/\ inc z Qplus_star, x [lt1 ne1]. move: (Qplus_or_sr_bis lt1) => [xq yq]. suff:glt Qplus_or x z /\ glt Qplus_or z y. move => [pa pb]; split => //;apply /Qplus_0_least1. move:(Qplus_0_least xq) (proj1 Qplus_or_tor) => aa or;order_tac. move:(Qplus_inc1 xq) => [sa sb]. move:(Qplus_inc1 yq) => [sa' sb']. rewrite /Qplus_middle. move/setX_P: (sa) => [pa pb pc1]; move/setC1_P: (pc1) => [pc pd]. move:pb pc1 pc pd; set a := P (rep x); set b := Q (rep x) => pb pe pc pd. move/setX_P: (sa') => [pa' pb' pc1']; move/setC1_P: (pc1') => []. move:pb' pc1'; set c := P (rep y); set d := Q (rep y) => pb' pe' pc' pd'. set num := (a *c d +c b *c c) ; set den := (b *c d) *c \2c. have nn: inc num Nat by rewrite/num;apply:NS_sum; fprops. have na1 := NS_prod pb pc'. have na2 := NS_prod pc pc'. have na3 := NS_prod pc pb'. have ra:inc (J num den) Qplus1. move:NS2 => n2. apply:setXp_i; first by exact. apply/setC1_P; split; first by apply:NS_prod => //. by apply: cprod2_nz; fprops;apply:cprod2_nz. have HH: a *c d eq; case: ne1; rewrite sb sb'. by apply/(Qplus_cc sa sa'). have [rb rc]: P (rep x) *c den h. move:(surjective_pr0 h) => h1. move:(image_smaller (proj1 h)); rewrite h1. rewrite /canon_proj; aw; rewrite Qplus_eq_sr -/Qplus /Qplus1 - cprod2_pr1. have pa: cardinal Nstar = cardinal Nat. symmetry; apply:card_setC1_inf;apply: infinite_Nat. rewrite - cprod2cr - cprod2cl pa aleph0_pr1 csquare_inf //. apply /infinite_setP; exact:infinite_Nat. Qed. Lemma Qplus_star_countable: countable_set Qplus_star. Proof. by apply:countable_sub Qplus_countable; apply:sub_setC. Qed. Definition Qplus01 := interval_oo Qplus_or Qplus_0 Qplus_1. Definition Qplus_star_o := induced_order Qplus_or Qplus_star. Definition Qplus_01_o := induced_order Qplus_or Qplus01. Lemma Qplus01_countable: countable_set Qplus01. Proof. apply:countable_sub Qplus_countable;rewrite / Qplus01/interval_oo. rewrite Qplus_or_sr;apply:Zo_S. Qed. (* Definition of eta like *) Definition eta_like0 r (E:=substrate r) := [/\ total_order r, countable_set E, (forall x, inc x E -> exists y, glt r y x), (forall x, inc x E -> exists y, glt r x y) & (forall x y, glt r x y -> exists z, glt r x z /\ glt r z y)]. Definition eta_like r := eta_like0 r /\ cardinal (substrate r) = aleph0. Lemma eta_like_pr1 r: eta_like0 r -> substrate r = emptyset \/ cardinal (substrate r) = aleph0. Proof. move => [ha hb hc hd he]. case: (emptyset_dichot (substrate r)) => hf; [by left | right]. case:(countable_finite_or_N hb) => // hg. move: (finite_set_torder_greatest ha hg hf) => [x [ /hd [y yp yq]]]. have /yq ysr: inc y (substrate r) by order_tac. case: (not_le_gt (proj1 ha) ysr yp). Qed. Lemma Qplus_star_o_sr: substrate Qplus_star_o = Qplus_star. Proof. move:Qplus_or_osr => [pa pb]. have s1: sub Qplus_star (substrate Qplus_or). rewrite pb; apply:sub_setC. exact: (iorder_sr pa s1). Qed. Lemma Qplus_star_eta_like0: eta_like0 (Qplus_star_o). Proof. move:Qplus_or_osr => [pa pb]. have s1: sub Qplus_star (substrate Qplus_or). rewrite pb; apply:sub_setC. move:(iorder_osr pa s1)(total_order_sub Qplus_or_tor s1). rewrite -/Qplus_star_o; move => [r1 r2] r3. move:Qplus_star_countable; rewrite - r2 => r4. split => //. + rewrite r2 => x xp; move:(Qplus_halfp xp) => [qa [qb pc]]. by exists (Qplus_half x); split => //; apply/iorder_gleP. + rewrite r2 => x xp; move:(Qplus_doublep xp) => [qa [qb pc]]. by exists (Qplus_double x); split => //; apply/iorder_gleP. + move => x y [/iorder_gle5P [xi yi l1] e1]. move:(Qplus_middlep (conj l1 e1)) => [ra [rb1 rb2] [rc1 rc2]]. move:(nesym rb2) => rb3. exists (Qplus_middle x y); split; split => //; apply/iorder_gleP => //. Qed. Lemma Qplus_star1: inc Qplus_1 Qplus_star. Proof. apply/setC1_P; split. apply: (Nat_to_Qplus_Q NS1). move/(Nat_to_Qplus_inj NS1 NS0) => eq; fprops. Qed. Lemma Qplus_star_eta_like: eta_like (Qplus_star_o). Proof. move:Qplus_star_eta_like0 => h; split => //. case: (eta_like_pr1 h) => // se. empty_tac1 Qplus_1; rewrite Qplus_star_o_sr. apply: Qplus_star1. Qed. Lemma Qplus_01_sr: substrate Qplus_01_o = Qplus01. Proof. move:Qplus_or_osr => [pa pb]. have s1: sub Qplus01 (substrate Qplus_or). rewrite pb. rewrite /Qplus01 /interval_oo Qplus_or_sr; apply:Zo_S. exact: (iorder_sr pa s1). Qed. Lemma Qplus_01_eta_like0: eta_like0 (Qplus_01_o). Proof. move:Qplus_or_osr => [pa pb]. have s1: sub Qplus01 (substrate Qplus_or). rewrite pb. rewrite /Qplus01 /interval_oo Qplus_or_sr; apply:Zo_S. move:(iorder_osr pa s1)(total_order_sub Qplus_or_tor s1). rewrite -/Qplus_01_o; move => [r1 r2] r3. move:Qplus01_countable; rewrite - r2 => r4. move: (proj1 Qplus_or_tor) => or. split => //. + rewrite r2 => x xa; move:(xa) => /Zo_P [sa [/Qplus_0_least1 hp sb]]. move:(Qplus_halfp hp) => [qa [qb pc]]. move/setC1_P: (qa) => [qa1 qa2]. exists (Qplus_half x); split => //; apply/iorder_gleP => //. apply /Zo_P; split; [by rewrite Qplus_or_sr | split ]. by apply / Qplus_0_least1. order_tac. + rewrite r2 => x xa; move:(xa) => /Zo_P [_ [sa sb]]. move: (Qplus_middlep sb) => [ha [h1 h2] [h3 h4]]. exists (Qplus_middle x Qplus_1); split => //. apply/iorder_gleP => //;apply/Zo_P; split => //. by rewrite Qplus_or_sr; move/setC1_P:ha => []. by split =>//; apply / Qplus_0_least1. + move => x y [/iorder_gle5P [xi yi l1] e1]. move:(Qplus_middlep (conj l1 e1)); set z:= (Qplus_middle x y). move => [sa [sb sc][sd se]]. have ha: glt Qplus_or Qplus_0 z by apply/ Qplus_0_least1. have hb: glt Qplus_or z Qplus_1. move/Zo_P:yi =>[_ [_ ya]]; order_tac. have zi: inc z Qplus01. by apply/Zo_P; split => //; rewrite Qplus_or_sr; move/setC1_P:sa => []. exists z; split; split => //;apply/iorder_gleP => //. Qed. Lemma Qplus_01_eta_like: eta_like (Qplus_01_o). Proof. move:Qplus_01_eta_like0 => h; split => //. case: (eta_like_pr1 h) => // se. have: glt Qplus_or Qplus_0 Qplus_1. apply/Qplus_0_least1; apply:Qplus_star1. move/ Qplus_middlep; set z:= Qplus_middle Qplus_0 Qplus_1. move => [pa pb pc]. empty_tac1 z; rewrite Qplus_01_sr; apply/Zo_P; split => //. by rewrite Qplus_or_sr; move /setC1_P:pa => []. Qed. Lemma Cantor_eta_pr r1 r2: eta_like r1 -> eta_like r2 -> r1 \Is r2. Proof. move => h1 h2. move: (esym(proj2 h1)); rewrite aleph0_pr1 => /card_eqP [f fp]. move: (esym(proj2 h2)); rewrite aleph0_pr1 => /card_eqP [g gp]. move: ( EP_fun_pr fp gp h1 h2) => h. by exists (EP_fun r1 r2 f g). Qed. Lemma Qstar_Is_Qstar01: Qplus_star_o \Is Qplus_01_o. Proof. apply: (Cantor_eta_pr Qplus_star_eta_like Qplus_01_eta_like ). Qed. End OrderType.