proposition: Lemma CantorL r r': worder r -> worder r' -> Corder_le r r' -> ~ Corder_le r' r -> Corder_lt r r'.
proof: Proof. move => wor1 wor2 h1 h2. move: (Cantor_not_le_aux wor2 h2) =>[a [asr ap al]]. pose pa x := seg_order r x \Is seg_order r' a. case: (all_exists_dichot2 pa (substrate r)) => // hu. have or2 := proj1 wor2. move:(proj2(seg_order_osr a or2)) => sr1. rewrite/Corder_lt; ex_tac; apply: orderIS. apply: (CantorK wor1 (seg_order_wor a wor2));rewrite /Corder_le sr1. move => x xsr; move: (h1 _ xsr) =>[y ysr is1]. case: (equal_or_not y a) => nay; first by case ap; rewrite - nay; hnf; ex_tac. case: (proj2 (worder_total wor2) _ _ ysr asr) => lay. have ys: inc y (segment r' a) by apply/segmentP. by ex_tac; rewrite seg_order_trans //. by case:(proj1 (CantorI wor1 wor2 asr hu) _ (conj lay (nesym nay)) _ xsr). move => y ys. have lya: glt r' y a by apply/segmentP. move: (arg1_sr (proj1 lya)) => ysr. move:(al y lya) => [x xsr /orderIS hx]; ex_tac;rewrite seg_order_trans //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)