proposition: Lemma CantorB_1 r x: worder r -> inc x (substrate r) -> r \Is (seg_order r x) -> False.
proof: Proof. move => wor xsr [f h]. move: (h) => [or or1 [[[ff _] _] sf tf] fi]. have xs: glt r (Vf f x) x. apply/segmentP;rewrite - (proj2(seg_order_osr x or)) - tf; Wtac. exact: (Cantor_aux wor (order_isomorphism_siso h) sf xs). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)