proposition: Lemma CantorN r r' (Ha := r \Is r')(Hb:= Corder_lt r' r) (Hc:= Corder_lt r r') : worder r -> worder r' -> [/\ [\/ Ha, Hb | Hc], Ha -> ~Hb /\ ~Hc, Hb -> ~Ha /\ ~Hc & Hc -> ~Hb /\ ~Ha ].
proof: Proof. move => wor1 wor2. have r1: Ha -> ~Hb. rewrite /Ha /Hb/Corder_lt => ha [x xsr hb]. exact: (CantorB wor1 xsr (orderIT ha (orderIS hb))). have r2: Ha -> ~Hc. rewrite /Ha /Hb/Corder_lt => ha [x xsr hb]. exact: (CantorB wor2 xsr (orderIS (orderIT hb ha))). have r3: Hb -> ~Hc. have or2 := (proj1 wor2). move =>[x xsr is1] [y ysr /orderIS [f fiso]]. have lt1: glt r' (Vf f x) y. move:(fiso) => [_ _ [[[ff _] _] sf tf] _]. apply/segmentP; rewrite - (proj2 (seg_order_osr y (or2))); Wtac. move: (arg1_sr (proj1 lt1)) => fxsr. move: (CantorA fiso xsr);rewrite (seg_order_trans or2 lt1) => is2. exact:(CantorB wor2 fxsr (orderIT (orderIS is1) is2)). split. * case: (p_or_not_p (Corder_le r r')) => ha; case: (p_or_not_p (Corder_le r' r)) => hb. + constructor 1;exact:(CantorK wor1 wor2 ha hb). + constructor 3;exact: (CantorL wor1 wor2 ha hb). + constructor 2;exact: (CantorL wor2 wor1 hb ha). + case: ha; exact: (CantorM wor1 wor2 hb). * by move => h; split; [ apply:r1 | apply: r2]. * by move => h; split => h'; [ case(r1 h') | case(r3 h) ]. * by move => h; split => h'; [ case (r3 h') | case(r2 h') ]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)