proposition: Lemma CantorD r x y: worder r -> inc x (substrate r) -> inc y (substrate r) -> (seg_order r x) \Is (seg_order r y) -> x = y.
proof: Proof. move => wor xsr ysr. suff H: forall a b, glt r a b -> (seg_order r a) \Is (seg_order r b) -> False. move =>h; ex_middle bad. case:(proj2(worder_total wor) x y xsr ysr) => le. case:(H _ _ (conj le bad) h). case:(H _ _ (conj le (nesym bad)) (orderIS h)). move => a b ltab {xsr ysr} ois. have or := proj1 wor. have asb: inc a (segment r b) by apply/segmentP. move: (seg_order_wor b wor)(seg_order_osr b or) => wor' [or' sr']. have asr': inc a (substrate (seg_order r b)) by ue. apply: (CantorB wor' asr'); apply: orderIS. by rewrite seg_order_trans. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)