proposition: Lemma CantorO r X: worder r -> sub X (substrate r) -> r \Is induced_order r X \/ (Corder_lt(induced_order r X) r).
proof: Proof. move => wor Xsr. case:(proj41(CantorN wor (induced_wor wor Xsr))) => h. - by left. - by right. - move: h =>[x]. rewrite (iorder_sr (proj1 wor) Xsr). rewrite /seg_order (iorder_trans _ (@sub_segment2 r X x)) => qa qb. have sb: sub (segment (induced_order r X) x) (segment r x). by move => t/segmentP/iorder_gltP [_ _ /segmentP]. case:(CantorC wor (Xsr _ qa) sb (orderIS qb)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)