proposition: Lemma sup_critical2 v: OIax2 u w0 g -> ordinalp u -> u +o \2o <=o v -> let A:= target (induction_defined0 (fun _ z => f z z) v) in critical_ordinal (\osup A) /\ v <=o (\osup A).
proof: Proof. move => ax; move: (ax) => [ax1 ax0 _ _]; move: (conj ax1 ax0) => ax1b. move: (induction_defined_pr0 (fun _ z => f z z) v) => /=. set h:= induction_defined0 _ _; move=> [sh sjh h0 hrec] ou lu2v. have ov:= (proj32 lu2v). have l2v: \2o <=o v by apply:(oleT (osum_M0le ou OS2) lu2v). have luv: u <=o v by apply:(oleT (osum_Mle0 ou OS2) lu2v). have pa: forall n, natp n -> [/\ ordinalp (Vf h n), u <=o (Vf h n), v <=o (Vf h n), Vf h n <o Vf h (csucc n) & n <o Vf h n]. apply: Nat_induction. have pa:=(olt_leT olt_02 l2v); have pb := (oleR ov). rewrite h0 //; split => //; rewrite (hrec _ NS0) h0. apply: ord_induction_p21d => //. move=> n nN [pa pb pc pd p]; rewrite (hrec _ nN). have pf:= (ord_induction_p21d ax1b pb (oleT l2v pc)). have [pf1 _] := pf. have aux:= oleT l2v pc. move: (proj32_1 pf) (oleT pb pf1) (oleT pc pf1)(oleT aux pf1) => a2 a3 a4 a5. split => //. by rewrite (hrec _ (NS_succ nN))(hrec _ nN); apply: ord_induction_p21d. by apply: ole_ltT pf; rewrite (succ_of_nat nN); apply /oleSltP. have pb: ordinal_set (target h). move=> t tt; move: ((proj2 sjh) _ tt); rewrite sh; move=> [x xs ->]. by move: (pa _ xs) => [ok _]. move: (OS_sup pb) => os. set y := union (target h). move: (sjh) => [fcth _]. have zt: inc v (target h) by rewrite -h0; Wtac => //;rewrite sh; apply: NS0. have net: nonempty (target h) by ex_tac. move: (ord_sup_ub pb zt); rewrite -/y => aux1. split; last by exact. have pc: u <o y. apply:(olt_leT _ (oleT lu2v aux1)). by move: (osum_Meqlt olt_02 ou); rewrite (osum0r ou) => le1. case: (ord_sup_inVlimit pb net) => yt. move: ((proj2 sjh) _ yt) => [v' vsh vv]. rewrite sh in vsh; move: (pa _ vsh) => [_ _ _ aux _]. rewrite -vv in aux. have pd:inc (Vf h (csucc v')) (target h ) by Wtac; rewrite sh; apply:NS_succ. case: (oltNge aux (ord_sup_ub pb pd)). apply: is_critical_pr => //. split => //; fprops; move => t tN; apply /(oltP os). move: (pa _ tN)=> [_ _ _ _ lt1]; apply: (olt_leT lt1). apply ord_sup_ub => //; Wtac; rewrite sh; fprops. move => x ux xy. move: (proj32_1 pc) => oy. move: (ord_induction_p10 fv (proj1 ax1b) ux) => [_ nf5]. rewrite (nf5 _ yt) -/y; apply: ord_ub_sup => //. move=> i /funI_P [j /(oltP oy) jy ->]. have fi: forall n, natp n -> forall m, natp m -> Vf h m <=o Vf h (m +c n). apply: Nat_induction. move=> m mN; rewrite (Nsum0r mN); apply: oleR. apply: pb; Wtac; ue. move=> n nN hr m mN; apply: (oleT (hr _ mN)). by rewrite (csum_nS _ nN);move: (pa _ (NS_sum mN nN))=> [_ _ _ [hh _] _]. move: (olt_sup pb xy) => [n nt [un _]]. move: (olt_sup pb jy) => [m mt [um _]]. move: ((proj2 sjh) _ nt)((proj2 sjh) _ mt)=> [N Nv u1] [M Mv u2]. rewrite sh in Nv Mv; move: (fi _ Nv _ Mv); rewrite -u2. move: (fi _ Mv _ Nv); rewrite -u1 csumC=> le1 le2. have le3:= oleT un le1. have le4:= oleT um le2. have ns: natp (M +c N) by apply: NS_sum. have ns1:= NS_succ ns. move: (ord_induction_p16 ax ux le3 le4) => pd; apply: (oleT pd). rewrite - hrec;[ apply: ord_sup_ub;[| Wtac; rewrite sh] |]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)