proposition: Lemma odiff_normal a: ordinalp a -> normal_ofs1 (odiff ^~ a) a.
proof: Proof. move => oa; apply/normal_ofs_equiv. have aux1:forall u v, a <=o u -> u <o v -> u -o a <o v -o a. move => u v au uv; move: (oleT au (proj1 uv)) => av. move: (odiff_pr au) (odiff_pr av) => [ou e1] [ov e2]. by move: uv; rewrite {1} e1 {1} e2; move /(osum_Meqltr ou ov oa). have aux:forall u v, a <=o u -> u <=o v -> u -o a <=o v -o a. move => u v au uv; move: (oleT au uv) => av. move: (odiff_pr au) (odiff_pr av) => [ou e1] [ov e2]. by move: uv; rewrite {1} e1 {1} e2; move /(osum_Meqler ou ov oa). split => // x lx ax. have ox:= (proj31 lx). set E := fun_image _ _. have ose: ordinal_set E. by apply:Os_funI=> v /(ointvP ox) [[_ ov _] vx]; apply: OS_diff. have m1: ordinal_ub E (x -o a). by move => t /funI_P [v /(ointvP ox) [av [vx _]] -> ]; apply: aux. have [sa sb]:= (odiff_pr (proj1 ax)). have os:= (OS_sup ose). have le1 := (ord_ub_sup sa m1). case: (oleT_el sa os) => le2; first by apply:oleA. move: (osum_Meqlt le2 oa); rewrite - sb => eq1. have: inc (\osup E) E. apply /funI_P;exists (a +o \osup E); last by symmetry; apply: odiff_pr1. by apply/(ointvP ox); split => //; apply:osum_Mle0. move => /funI_P [y /(ointvP ox) [e1 e2] eq]. move/(limit_ordinal_P): (lx) => [ _ h3]; move: (h3 _ e2) => h4. have h5 :=(oltS (proj32 e1)). have h6:= (aux1 _ _ e1 h5). have se: (inc ((osucc y) -o a) E). apply/funI_P; exists (osucc y) => //; apply/(ointvP ox); split => //. exact: (oleT e1 (proj1 h5)). by move: (ord_sup_ub ose se); rewrite eq => /(oltNge h6). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)