proposition: Lemma sup_critical3 A: OIax2 u w0 g -> nonempty A -> (forall x, inc x A -> critical_ordinal x) -> critical_ordinal (\osup A).
proof: Proof. move => ax; move: (ax) => [ax1 ax0 _ _]; move: (conj ax1 ax0) => ax1b. move => neA hA. have oA: ordinal_set A by move=> x xA; move: (hA _ xA) =>[ /proj32]. case: (inc_or_not (union A) A) => nuaa; first by apply: hA. case: (ord_sup_inVlimit oA neA) => ca; first by apply: hA. have osA: ordinalp (\osup A) by apply: OS_sup. move: neA => [t tA];move: (ord_sup_ub oA tA) => lty. move: (hA _ tA) => [ot p3 p4]. have ou:=oleT ot lty. have ou':=(olt_leT p3 lty). apply: is_critical_pr => // x ux xu. rewrite (proj2 (ord_induction_p10 fv ax1 ux) _ ca); apply: ord_ub_sup => //. move => i /funI_P [j ji ->]. have [z [z1 z2 z3]]: exists z, [/\ x <=o z, j <=o z & z <o union A]. move: (proj32 ux) (Os_ordinal osA ji) => ox oj. move: (oleR oj)(oleR ox) => lej lex. case: (oleT_ee ox oj) => le. by exists j; split => //; apply/(oltP osA). by exists x. move /(oltP osA): (z3) => z4. move: ca => [_ _ h]; move: (h z z4); move /(oltP osA) => h1. move: (olt_sup oA h1) => [v vA zv]. have lt1:=(oltS (proj32 z1)). have lt2:= (olt_ltT lt1 zv). have le4:= (oleT z2 (proj1 lt2)). have le3:= oleT ux z1. apply: (oleT (ord_induction_p16 ax ux z1 le4)). by move:(hA _ vA)=> [_ _ H]; rewrite (H _ le3 lt2); apply: ord_sup_ub. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)