proposition: Lemma CantorA r r' f x (y := Vf f x): order_isomorphism f r r' -> inc x (substrate r) -> (seg_order r x) \Is (seg_order r' y).
proof: Proof. move => h xsr. move: (order_isomorphism_siso h) => fsi. move: h => [or1 or2 [bf sf tf] fi]. have ff := proj1 (proj1 bf). move: (seg_order_osr x or1) =>[ra rb]. move: (seg_order_osr y or2) =>[rc rd]. have sSx: sub (segment r x) (source f) by rewrite sf; apply: sub_segment. have sSy: sub (segment r' y) (target f) by rewrite tf; apply: sub_segment. have xsf: inc x (source f) by ue. have ax0 u: inc u (segment r x) -> inc (Vf f u) (segment r' y). move=> ux;by apply/segmentP; apply/(fsi _ _ (sSx _ ux) xsf); apply/segmentP. have ax: restriction2_axioms f (segment r x) (segment r' y). by split => // t; move /(Vf_image_P ff sSx) => [u ux ->]; apply: ax0. case: (restriction2_prop ax). set g := restriction2 _ _ _ => fg sg tg. have bg: bijection g. split; first exact: (restriction2_fi (proj1 bf) ax). split => //; rewrite tg sg => u ust. move: (proj2 (proj2 bf) u (sSy _ ust))=>[v vsf eq1]. have vSx: inc v (segment r x). by apply/segmentP; apply/(fsi _ _ vsf xsf); rewrite - eq1; apply/segmentP. by ex_tac; rewrite (restriction2_V ax vSx). exists g; split => //; first by hnf; rewrite rb rd. move => u v; rewrite sg => usx vsx; move: (ax0 _ usx)(ax0 _ vsx) => usy vst. rewrite (restriction2_V ax usx)(restriction2_V ax vsx). apply: (iff_trans (iorder_gle0P r usx vsx)). apply: (iff_trans (fi u v (sSx _ usx) (sSx _ vsx))). by apply: iff_sym; apply: iorder_gle0P. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)