proposition: Lemma aleph_succ_P1 x: ordinalp x -> (forall t, inc t (aleph_succ_comp x) <-> ((\aleph x) <=o t /\ t <o (\aleph (osucc x)))).
proof: Proof. move => ox t. move: (aleph_lt_lto (oltS ox)) => lt1. move: (lt1) => [[oy oy' _] _]. split. move /setC_P => [ta tb]. have ot:= (Os_ordinal oy' ta). split; last by apply /oltP0;split => //. by case: (oleT_el oy ot) => //;move/oltP0 => [_ _]. move => [[p1 p2 p3] p4]; apply /setC_P; split => //. by move /(oltP0) : p4 => [_ _]. move => p5; exact:(ordinal_irreflexive p2 (p3 _ p5)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)