proposition: Lemma urank_union a x : ordinalp a -> inc x (universe a) -> inc (union x) (universe a) /\ (urank a (union x)) = (opred (urank a x)).
proof: Proof. move => oa xa. move: (urank_pr1 oa xa) => [pa pb]. move: (pb) => [orx qb qc]. set b := urank a x. set c := opred (urank a x). have pc: forall y, inc y x -> inc y (universe a) /\ (urank a y) <o b. by move => y /(urank_inc oa xa). have osb: ordinal_set b by move => t /(Os_ordinal orx). have pd: c <=o b. by apply: ord_ub_sup => // t tb; move/(oltP orx): tb => []. have oc:= proj31 pd. have aux: forall u, u <o b -> u <=o c. move => u ub;have ub':=(olt_i ub); have ou'':= (Os_ordinal orx ub'). split => //;apply: (setU_s1 ub'). have pe: sub (union x) (universe c). move => t /setU_P [z za zb]. have p3: sub z (universe a) by move: (pc _ zb) => [/(universe_trans oa)]. move: (urank_inc oa xa zb) => [_] /aux /universe_inc2; apply. by move: (urank_pr oa p3) => [_ [s1 s2 s3]];apply: s2. have pf :inc (union x) (universe a). by apply: (universe_inc1 (ole_ltT pd pa)); apply /setP_P. move: (urank_pr oc pe) => [s1 s2]. move: (urank_pr oa (universe_trans oa pf)) => [_ s4]. move: (urank_uniq s2 s4) => eq. move: s1 s2; rewrite eq; set d := urank a (union x) => dc pg. split => //; clear s4 eq; apply: oleA => //. move: (urank_powerset oa pf) => [q1]. move:(urank_pr1 (OS_succ oa) q1) => [_ rp1]. move: (q1); rewrite (universe_succ oa) => /setP_P /(urank_pr oa) [_ rp2]. rewrite (urank_uniq rp2 rp1) => h. have sa: sub x (\Po (union x)). move => t tx; apply /setP_P => s st; union_tac. move: (urank_sub (OS_succ oa) q1 sa) => [q3]. rewrite - (urank_uniq2 oa (OS_succ oa) xa q3) h -/d /c -/b => bsd. apply: (ord_ub_sup (proj31 dc)). by move => t /(oltP (proj31 pb)) ha; apply /oltSleP; apply: (olt_leT ha bsd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)