proposition: Lemma Cantor_not_le_aux r r' (p := fun y => exists2 x, inc x (substrate r) & seg_order r x \Is seg_order r' y): worder r' -> ~ Corder_le r' r -> exists a, [/\ inc a (substrate r'), ~ p a & forall b, glt r' b a -> p b].
proof: Proof. move => wor2 h2. set E := Zo (substrate r') (fun y => ~ p y). have ser: sub E (substrate r') by apply: Zo_S. have neE: nonempty E. case: (all_exists_dichot1 p (substrate r')). move =>h3; case: h2 => y /h3 [x xst /orderIS xl]; ex_tac. by move => [x ha hb]; exists x; apply: Zo_i. move: (worder_prop wor2 ser neE) =>[a /Zo_P [asr h] al]. exists a; split => //b ltab. move:(arg1_sr (proj1 ltab)) => bsr. ex_middle bad; have /al le2: inc b E by apply: Zo_i. case: (not_le_gt (proj1 wor2) le2 ltab). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)