proposition: Lemma aleph_succ_pr3 x y: ordinalp x -> ordinalp y -> x = y \/ disjoint (aleph_succ_comp x) (aleph_succ_comp y).
proof: Proof. move=> ox oy. case: (equal_or_not x y); [by left | move => h0; right;apply /set0_P => t]. move /setI2_P => [] /(aleph_succ_P1 ox) [pa pb] /(aleph_succ_P1 oy) [pc pd]. case: h0; apply: oleA; apply /oltSleP. by move: (aleph_lto_lt ox (OS_succ oy) (ole_ltT pa pd)). by move: (aleph_lto_lt oy (OS_succ ox) (ole_ltT pc pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)