proposition: Lemma CantorI r r' y: worder r -> worder r' -> inc y (substrate r') -> (forall x, inc x (substrate r) -> ~ seg_order r x \Is seg_order r' y) -> (forall y', glt r' y y' -> forall x, inc x (substrate r) -> ~ seg_order r x \Is seg_order r' y') /\ forall x, inc x (substrate r) -> ~ seg_order r x \Is r'.
proof: Proof. move => wor1 wor2 ysr yp;split. move => y' ly1 x' xsr' is1. move: (proj2 (CantorG wor1 wor2 is1) y ly1) =>[x /proj1/arg1_sr xsr h]. case: (yp x xsr h). move => x xsr is1. move:(orderIS is1) => [f ff]; move: (ff) =>[_ _ [[[fuf _] _]sf tf] _]. have lt1: glt r (Vf f y) x. apply/segmentP; rewrite - (proj2 (seg_order_osr x (proj1 wor1))); Wtac. case: (yp _ (arg1_sr (proj1 lt1))). by move:(orderIS (CantorA ff ysr)); rewrite (seg_order_trans (proj1 wor1)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)