proposition: Lemma CantorC_1 r x X: worder r -> inc x (substrate r) -> sub X (segment r x) -> r \Is (induced_order r X) -> False.
proof: Proof. move => wor xsr Xsk [f h]. move: (h) => [or or1 [[[ff _] _] sf tf] fi]. have xs: glt r (Vf f x) x. apply/segmentP; apply: (Xsk). rewrite - (iorder_sr or (sub_trans Xsk (@sub_segment r x))) - tf; Wtac. exact: (Cantor_aux wor (order_isomorphism_siso h) sf xs). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)