proposition: Lemma CantorB r x: worder r -> inc x (substrate r) -> r \Is (seg_order r x) -> False.
proof: Proof. move => wor xsr fiso. have or := proj1 wor. set E := Zo (substrate r) (fun z => r \Is (seg_order r z)). have ses: sub E (substrate r) by apply: Zo_S. have ne: nonempty E by exists x; apply: Zo_i. move: (worder_prop wor ses ne) =>[a /Zo_P [asr isa] al] {fiso xsr}. move: (seg_order_osr a or) => [oo eq1]. move: (isa) => [f ff]; move:(ff) => [_ _ [bf sf tf] _]. have asf: inc a (source f) by ue. move: (Vf_target (proj1 (proj1 bf)) asf); rewrite tf eq1 => /segmentP lt1. move: (CantorA ff asr); rewrite (seg_order_trans or lt1) => gp. move:(orderIT isa gp) => ci. have:inc (Vf f a) E by apply: (Zo_i (arg1_sr (proj1 lt1))). move/al => be;exact: (not_le_gt or be lt1). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)