proposition: Lemma CantorG r r' x y: worder r -> worder r' -> (seg_order r x) \Is (seg_order r' y) -> (forall x', glt r x' x -> exists2 y', glt r' y' y & (seg_order r x') \Is (seg_order r' y')) /\ (forall y', glt r' y' y -> exists2 x', glt r x' x & (seg_order r x') \Is (seg_order r' y')).
proof: Proof. move => wor1 wor2 [f fiso]. move: (proj1 wor1) (proj1 wor2)=> or1 or2. move: (fiso) =>[_ _ [bf sf tf]_]. move: (seg_order_wor x wor1) (seg_order_osr x (proj1 wor1)) => wor1x [_ sr1x]. move: (seg_order_wor y wor2) (seg_order_osr y (proj1 wor2)) => wor2y [_ sr2y]. rewrite sr1x in sf. rewrite sr2y in tf. have ff: function f by fct_tac. suff aux x': glt r x' x -> (seg_order r x') \Is (seg_order r' (Vf f x')). split. move => x' lt1. have x'sf: inc x' (source f) by rewrite sf; apply/segmentP. have lt2 :glt r' (Vf f x') y by apply/segmentP; Wtac. exists (Vf f x'); [ exact | by apply: aux]. move => y' lt3. have y'tf: inc y' (target f) by rewrite tf; apply/segmentP. move: (proj2 (proj2 bf) y' y'tf) =>[x' x'sf ->]. have lt4: glt r x' x by apply /segmentP; rewrite - sf. exists x' => //; exact: (aux _ lt4). move => lt1. have x'sf: inc x' (source f). by rewrite sf; apply/segmentP. have lt2 :glt r' (Vf f x') y by apply/segmentP; Wtac. have ii1: inc x' (substrate (seg_order r x)) by rewrite sr1x; apply/segmentP. move: (CantorA fiso ii1); rewrite seg_order_trans // seg_order_trans //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)