proposition: Lemma CantorM r r': worder r -> worder r' -> ~ Corder_le r' r -> Corder_le r r'.
proof: Proof. move => wor1 wor2 h2; ex_middle h1. move: (Cantor_not_le_aux wor1 h1) => [a [asr ap al]]. move: (Cantor_not_le_aux wor2 h2) => [b [bsr bp bl]]. suff: seg_order r a \Is seg_order r' b. move => h; case: bp; ex_tac. move: (seg_order_wor a wor1) (seg_order_wor b wor2) => sa sb. move: (proj2(seg_order_osr a (proj1 wor1))) => sra. move: (proj2(seg_order_osr b (proj1 wor2))) => srb. move: (proj1 wor1) (proj1 wor2) => or1 or2. apply: (CantorK sa sb). move => u; rewrite sra srb => /segmentP lt1. move:(arg1_sr (proj1 lt1)) => usr. move:(al _ lt1) =>[v vsr /orderIS is1]. case: (total_order_pr1 (worder_total wor2) bsr vsr) => lt2. - pose pra z := seg_order r z \Is seg_order r' b. case: (all_exists_dichot2 pra (substrate r)) => // hu. by case:(proj1 (CantorI wor1 wor2 bsr hu) v lt2 u usr). - by move/segmentP: (lt2) => vsb; ex_tac; rewrite !seg_order_trans //. - by rewrite - lt2 in is1; case: bp; ex_tac. move => v; rewrite sra srb => /segmentP lt2. move:(bl _ lt2) =>[u usr /orderIS is1]; move:(arg1_sr (proj1 lt2)) => vsr. case: (total_order_pr1 (worder_total wor1) asr usr) => lt1. - pose pra z := seg_order r' z \Is seg_order r a. case: (all_exists_dichot2 pra (substrate r')) => // hu. by case: (proj1 (CantorI wor2 wor1 asr hu) u lt1 v vsr). - by move/segmentP: (lt1) => usa; ex_tac; rewrite !seg_order_trans //. - by rewrite - lt1 in is1; case: ap; ex_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)