proposition: Lemma Cantor_eta_pr7: OT_opposite 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: (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.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)