proposition: Lemma Cantor_eta_pr6: 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]. set r := BQ_int01_order. 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; aw. apply /setX2_P; split => //; aww; order_tac. by move => hg; case: (proj2 yp); rewrite - hg; aw. + 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; aw. apply /setX2_P; split => //; aww; order_tac. by move => hg; case: (proj2 yp);rewrite hg; aw. + 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. by 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 => //; aww;order_tac. have zc: Vg z1 C1 = z by rewrite /z1; aw. have zd: Vg z1 C0 = Vg x C0 by rewrite /z1; aw. 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 => //; aww; order_tac. have zc: Vg z1 C0 = z by rewrite /z1; aw. 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.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)