proposition: Lemma Cantor_etaP r: order r -> (eta_like r <-> order_type_of r = Cantor_eta).
proof: Proof. move => or;split; first by apply:Cantor_eta_prop2. move: eta_likeQp_int01 => [[pa _ pb pc pd] pe]. move => h;move: (OT_prop0 or) (OT_prop0 (proj1 pa)). rewrite -/Cantor_eta h => sa sb; move: (orderIT (orderIS sa) sb). move => [f [_ _ fp sincf]] {h sa sb}. have csr: cardinal (substrate r) = aleph0. by rewrite - pe; apply /card_eqP; exists f. have ccsr:= (aleph0_countable csr). move: fp => [bf sf tf]; move: (proj1 (proj1 bf)) => ff. split => //; split => //. + split => // x y; rewrite - sf => xsr ysr. move: (Vf_target ff xsr) (Vf_target ff ysr); rewrite tf => xa ya. case: (proj2 pa _ _ xa ya) => h. by left; move/(sincf x y xsr ysr): h. by right; move/(sincf y x ysr xsr): h. + move => x; rewrite - sf => xsr; move: (Vf_target ff xsr); rewrite tf => xa. move:(pb (Vf f x) xa) => [z ylx]. have: inc z (substrate BQ_int01_order) by order_tac. rewrite - tf => zt; move: (bij_surj bf zt) => [y ysf yv]; exists y. move:ylx; rewrite yv; move => [ra rb]; split; last by dneg hh; rewrite hh. by apply /(sincf y x ysf xsr). + move => x; rewrite - sf => xsr; move: (Vf_target ff xsr); rewrite tf => xa. move:(pc (Vf f x) xa) => [z ylx]. have: inc z (substrate BQ_int01_order) by order_tac. rewrite - tf => zt; move: (bij_surj bf zt) => [y ysf yv]; exists y. move:ylx; rewrite yv; move => [ra rb]; split; last by dneg hh; rewrite hh. by apply /(sincf x y xsr ysf). + move => x y [lxy nxy]. have: inc x (substrate r) by order_tac. have: inc y (substrate r) by order_tac. rewrite - sf => ysr xsr. move/(sincf x y xsr ysr): lxy => le1. have: glt BQ_int01_order (Vf f x) (Vf f y). by split => //; move /(proj2 (proj1 bf) _ _ xsr ysr). move /pd => [u [[ua ub] [uc ud]]]. have: inc u (substrate BQ_int01_order) by order_tac. rewrite - tf => zt; move: (bij_surj bf zt) => [z zsr zv]; exists z. rewrite zv in ua ub uc ud. split; split. + by apply /(sincf _ _ xsr zsr). + clear ud;dneg hh; ue. + by apply /(sincf _ _ zsr ysr). + dneg hh; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)