proposition: Lemma OT_le_not_order (r1 := Cantor_eta) (r2 := Cantor_eta +t \1t): [/\ r1 <=t r2, r2 <=t r1 & r1 <> r2].
proof: Proof. have ot1: order_type r1 by exact:(OT_prop1 (proj1 BQ_int01_or_osr)). have ot2 := OT_1_order_type. have p1:=(proj1 (OTsum_Mle0 ot1 ot2)). have p3 := (nesym Cantor_eta_pr2). split => //; rewrite /r1 - Cantor_eta_pr4; apply /(OTsum_Mle2 ot1). apply:(OT_1_least_nz ot1) => /esym h. move: set0_wor =>[[qa _] qb]. move:(Cantor_etaP qa); rewrite OT_set0 => p; move/p: h => /proj2. by rewrite qb cardinal_set0 => res; apply: aleph0_nz. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)