proposition: Lemma Cantor_eta_pr3: \1t +t Cantor_eta <> Cantor_eta.
proof: 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] //. by move/set1_P => /pr1_def h; case nexy;apply: pair_exten; fprops; aw. by case: C0_ne_C1; rewrite - sa - sd. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)