proposition: Lemma CantorK r r': worder r -> worder r' -> Corder_le r r' -> Corder_le r' r -> r \Is r'.
proof: Proof. move => wor1 wor2 h1 h2. move: (proj1 wor1) (proj1 wor2) => oe1 or2. pose p x y := seg_order r x \Is seg_order r' y. pose f x := (select (p x) (substrate r')). have fp x: inc x (substrate r) -> p x (f x) /\ inc (f x) (substrate r'). move => xsr. have sv: singl_val2 (inc^~ (substrate r')) (p x). move => u v /= usr pu vsr pv. exact:(CantorF wor2 usr vsr pu pv). by move: (select_pr (h1 x xsr) sv). have ax: lf_axiom f (substrate r) (substrate r'). by move => t /fp []. have bp: bijection_prop (Lf f (substrate r) (substrate r')) (substrate r) (substrate r'). hnf; saw; apply: (lf_bijective ax). move => u v usr vsr sf. move: (fp u usr) (fp v vsr) =>[sa sb][sc sd]. rewrite - sf in sc. exact: (CantorF wor1 usr vsr (orderIS sa) (orderIS sc)). move => y ysr; move:(h2 _ ysr) => [x xsr /orderIS xp]; ex_tac. move: (fp x xsr) => [qa qb]. exact: (CantorF wor2 ysr qb xp qa). exists (Lf f (substrate r) (substrate r')); split => //. hnf; aw; move => u v usr vsr; rewrite !LfV//. move:(fp _ usr) (fp _ vsr) =>[sa sb][sc sd]. exact: (proj1 (CantorH wor1 wor2 usr sb vsr sd sa sc)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)