proposition: Lemma Cantor_eta_pr5: Cantor_eta +t \1t +t Cantor_eta = Cantor_eta.
proof: Proof. move:BQ_int01_or_osr => [or1 sr1]. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. set r := BQ_int01_order. 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 - aleph0_pr2 sr4 -[cardinal _]/(_ +c _) - csum2cr pe - csum2cl sr3. congr (_ +c aleph0). rewrite -[cardinal _]/(_ +c _) - csum2cr - csum2cl OT_cardinal_1 pe. by rewrite aleph0_plus1. 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 <q \1q. rewrite - BQdouble_half2; apply:(BQsum_Mps ra QpsSh2 ). by rewrite /T sr1; apply/Zo_P. move: C0_ne_C1 => 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; saw; apply/orsum2_gleP; split => //. by 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; saw; 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); saw; constructor 1; split => //. + by rewrite - px - ppx => /pr1_def /pr1_def. + apply/(orsum2_gleP); split => //; constructor 1; saw. by apply/(orsum2_gleP); saw; 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.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)