proposition: Lemma proposition_S E (A := substrate (one_aleph_of E)): Sinfinite E -> [/\ Saleph A, ~ E <s A & ~ A <s E].
proof: Proof. move => einf. case: (one_aleph_of_prop E);rewrite -/A => sa sb sc; split => //. split; last by exists (one_aleph_of E). move => Ad. have [n nN ean] : exists2 n, natp n & A \Eq n. move:Nat_order_wor => [wo2 sr2]. case:(isomorphism_worder2 sa wo2). - move => [f [_ _]]; rewrite -/A sr2 => fp _. by case: Ad => _; case; exists f. - rewrite -/A; move =>[x xA [f [_ _]]]. move: (@sub_segment (one_aleph_of E) x); set u := segment _ _ => s1. rewrite (iorder_sr (proj1 sa) s1) sr2 => bf _. have h: Nat <=s A by apply/set_leP; exists u => //; apply: EqS; exists f. case:(set_lt_leT Ad h) => _; case; apply: EqR. - move => [n ]; rewrite sr2 => nN. rewrite /seg_order (segment_Nat_order1 nN). have ha: sub n (substrate Nat_order) by rewrite sr2 => t / (NS_inc_nat nN). move =>[f [_ _ ]]; rewrite (iorder_sr (proj1 wo2) ha) => fp _. by exists n => //; apply: EqS; exists f. case: (set_compare_to_finite E nN) => lt. by move:(set_lt_i2 lt (EqS ean)). move: (set_le_i1 lt (EqS ean)) => lt1; case: sb. by split => // aa; move:(set_lt_i1 Ad aa). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)