proposition: Lemma CantorC 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 Xsr iso. set E := Zo (substrate r) (fun z => exists2 X, sub X (segment r z) & r \Is (induced_order r X)). have ses: sub E (substrate r) by apply: Zo_S. have ne: nonempty E. by exists x; apply: (Zo_i xsr); exists X. clear x X xsr Xsr iso. move: (worder_prop wor ses ne) =>[x /Zo_P [xsr [X Xsr [f fiso]]] xl]. move:(fiso) => [or _ [bf sf tf] _]. have asf: inc x (source f) by ue. move: (sub_trans Xsr (@sub_segment r x)) => Xs. move: (proj2(seg_order_osr x or)) => eq1. move: (iorder_sr or Xs) => eq2. move: (Vf_target (proj1 (proj1 bf)) asf); rewrite tf eq2 => inc1. move /segmentP: (Xsr _ inc1) => lt1. move: (arg1_sr (proj1 lt1)) => fxsr. suff: inc (Vf f x) E by move/ xl => le1;exact: (not_le_gt or le1 lt1). move: (CantorA fiso xsr) =>[g]. set A := (segment (induced_order r X) (Vf f x)). set B := (segment r (Vf f x)). have sAB: sub A B. by move=> t/segmentP/iorder_gltP [ _ _/segmentP]. have sAX: sub A X by move => t/segmentP /iorder_gltP []. have sr1: sub (segment r x) (substrate r) by apply: sub_segment. have sr2:= sub_trans sAX Xs. rewrite /seg_order (iorder_trans _ sAX). move =>[or1 or2]; rewrite iorder_sr // iorder_sr //; move => [bg sg tg] pb. have fg: function g by fct_tac. have Xsg: sub X (source g) by rewrite sg. move: (restriction1_fb (proj1 bg) Xsg) => bh. move:(restriction1_prop fg Xsg) =>[fh sh th]. have ss: sub (Vfs g X) A by rewrite - tg; apply: fun_image_Starget1. have hiso: order_isomorphism (restriction1 g X) (induced_order r X)(induced_order r (Vfs g X)). move:(iorder_osr or Xs) =>[sa sb]. move:(iorder_osr or (sub_trans ss sr2)) =>[sc sd]. split => //; first by rewrite sb sd. move => u v; rewrite sh => ux vx. rewrite (restriction1_V fg Xsg ux) (restriction1_V fg Xsg vx). apply: (iff_trans (iorder_gle0P r ux vx)). move: (pb u v (Xsg _ ux) (Xsg _ vx)) => aux. move:(iff_trans (iff_sym (iorder_gle0P r (Xsr _ ux) (Xsr _ vx))) aux) => h. have se: inc (Vf g u) (Vfs g X) by apply/(Vf_image_P fg Xsg); exists u. have si: inc (Vf g v) (Vfs g X) by apply/(Vf_image_P fg Xsg); exists v. have sj: inc (Vf g u) A by Wtac. have sk: inc (Vf g v) A by Wtac. split. by move/h => /iorder_gleP [qa qb qc]; apply/iorder_gleP. by move/iorder_gleP =>[_ _ lr4]; apply /h; apply/iorder_gleP. apply: (Zo_i fxsr); exists (Vfs g X). exact: (sub_trans ss sAB). exists (restriction1 g X \co f). exact:(compose_order_is fiso hiso). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)