proposition: Lemma one_aleph_of_prop E: aleph_of E (one_aleph_of E).
proof: Proof. rewrite /one_aleph_of. set r := worders_order E. set Z := Zo _ _; set X0 := the_least _; set X1 := Yo _ _ _. have pa: ~ (worders_quo E) <s E. apply/set_lt_notP => f fp. have /worders_qle_prop4//: (worders_quo E) <=s E by exists f. move:(worders_qle_order E) => [orQ srQ]. have wor := (worders_qle_prop3 E). have ZQ: sub Z (substrate (worders_order E)) by rewrite srQ; apply: Zo_S. pose s X := [/\ segmentp r X, ~ X <s E & forall t, inc t X -> (segment r t) <s E]. have ra: nonempty Z -> s (segment r X0). move => ze. move: (iorder_osr orQ ZQ) =>[oZ sZ]. move:(the_least_pr oZ (proj2 wor Z ZQ ze)); rewrite -/X0. case; rewrite sZ; move =>/Zo_P[xQ hx1] etc. have ss: segmentp r (segment r X0) by apply: segment_segment. split => // t/segmentP ltr. case: (inc_or_not t Z) => itz. move:(etc _ itz) => /iorder_gleP [_ _Ø] le; order_tac. by ex_middle bad; case: itz; apply: Zo_i;first by rewrite - srQ; order_tac. have rb: ~ (nonempty Z) -> s (worders_quo E). split => //; first by rewrite - srQ; apply: substrate_segment. move => t tsr; ex_middle bad. case: (inc_or_not t Z) => itz; first by case :H; ex_tac. by case: itz; apply: (Zo_i tsr). have [qa qb qc]: s X1 by rewrite /X1; Ytac foo; fprops. move:(proj1 qa) => sr2; move: (induced_wor wor sr2) => wo2. split => //; rewrite (iorder_sr orQ sr2) => //; case. move => [f [ff sf tf]]. move:(Eq_src_range ff); rewrite sf => eq2. case; apply: (EqT eq2). have eq1 := (iorder_sr orQ sr2). move:(Imf_Starget (proj1 ff)); rewrite tf => ss1. move:(ss1); rewrite - {1} eq1 => ss2. case: (isomorphism_worder_sub wo2 ss2)O. set w := iso_seg_fun _ _ => ws. move:(proj1 ws); rewrite eq1 => ss3. rewrite (iorder_trans _ ss1) (iorder_trans _ ss3) => is1. have eqxi : Imf f \Eq (target w). move: is1 => [_ _ kp _]; move: kp. rewrite (iorder_sr orQ (sub_trans ss1 sr2)). rewrite (iorder_sr orQ (sub_trans ss3 sr2))=> is1. exact: (equipotent_bp is1). case: (well_ordered_segment (induced_wor wor sr2) ws). by rewrite eq1 => <-. move => [x]. rewrite (iorder_sr orQ sr2) => x1X. rewrite (segment_induced_a qa x1X) => vw. case: (proj2 (qc _ x1X)); rewrite - vw; exact: (EqS(EqT eq2 eqxi)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)