proposition: Lemma CantorH r r' x x' y y': worder r -> worder r' -> inc x (substrate r) -> inc y (substrate r') -> inc x' (substrate r) -> inc y' (substrate r') -> (seg_order r x) \Is (seg_order r' y) -> (seg_order r x') \Is (seg_order r' y') -> ((gle r x x' <-> gle r' y y' )/\ (glt r x x' <-> glt r' y y')).
proof: Proof. move => wor1 wor2 xsr ysr xsr' ysr' iso1 iso2. move:(proj1 wor1)(proj1 wor2) => or1 or2. have res1: x = x' -> y = y'. move => ea; rewrite -ea in iso2. exact: (CantorF wor2 ysr ysr' iso1 iso2). have res2: y = y' -> x = x'. move => ea; rewrite -ea in iso2. exact: (CantorF wor1 xsr xsr' (orderIS iso1) (orderIS iso2)). have res5: glt r x x' -> glt r' y y'. move => lt1. move: (proj1 (CantorG wor1 wor2 iso2) _ lt1) => [z lt2 is3]. have zsr:= (arg1_sr (proj1 lt2)). move: (orderIT (orderIS is3) iso1) => iso3. by rewrite- (CantorF wor2 zsr ysr is3 iso1). have res4: glt r x' x -> glt r' y' y. move => lt1. move: (proj1 (CantorG wor1 wor2 iso1) _ lt1) => [z lt2 is3]. have zsr:= (arg1_sr (proj1 lt2)). move: (orderIT (orderIS is3) iso2) => iso3. by rewrite (CantorF wor2 ysr' zsr iso2 is3). case: (equal_or_not x x') => ee. rewrite ee (res1 ee); split; [ by split => _; order_tac | by split; case]. case:(proj2 (worder_total wor1) x x' xsr xsr') => le1. by split; split => // _; move:(proj1 (res5 (conj le1 ee))). move: (res4 (conj le1 (nesym ee))) => ltyy; move: (proj1 ltyy)=> leyy. split; split => h. - case:(not_le_gt or2 leyy (res5 (conj h ee))). - case: ee; exact:(res2(proj44 or2 _ _ h leyy)). - case:(not_le_gt or1 le1 h). - case:(not_le_gt or2 leyy h). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)