proposition: Lemma Cantor_eta_pr4: Cantor_eta +t Cantor_eta = Cantor_eta.
proof: 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_order. 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 _]/(_ +c _) - csum2cr - csum2cl 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.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)