proposition: Lemma normal_ofs_equiv f u: normal_ofs1 f u <-> normal_ofs2 f u.
proof: Proof. rewrite /normal_ofs1/ normal_ofs2. split; move=> [p2 p3]; split => //. move=> x lx ux. have [[ou ox _] _ ]:= ux; have uu := oleR ou. set X := (ordinal_interval u x). have p4: forall x, inc x X -> u <=o x by move=> y /(ointvP ox) []. have p5: nonempty X by exists u; apply /ointvP. rewrite (p3 _ p4 p5 ) (ointv_sup1 ux lx) //. move=> X Xp neX. have p1:=(ofs_sincru p2). set Y:= (fun_image X f). have p4: ordinal_set Y by apply:Os_funI => z zX; apply: p1; apply: Xp. have p7: ordinal_set X by move=>j /Xp[]. case: (inc_or_not (union X) X) => sX. have sf: inc (f (union X)) Y by apply /funI_P; ex_tac. have le1:= (ord_sup_ub p4 sf). have p5: ordinalp (f (union X)) by case: le1. have p6: (forall i, inc i Y -> i <=o (f (union X))). move=> i /funI_P [z zX ->]. have h:= (ord_sup_ub p7 zX). case:(ole_eqVlt (ord_sup_ub p7 zX)). move ->;apply:oleR. fprops. by move => h2; case: (p2 _ _ (Xp _ zX) h2). exact:(oleA (ord_ub_sup p5 p6) le1). case: (ord_sup_inVlimit p7 neX) => // ls. have ltus: u <o \osup X. move: (neX) => [x xX]; apply: (ole_ltT (Xp _ xX)). split; [ exact: (ord_sup_ub p7 xX) | dneg w; ue ]. rewrite (p3 _ ls ltus). have oos := (proj32_1 ltus). have sXoi: sub X (ordinal_interval u (union X)). move=> t tX; apply /(ointvP oos). by split; [ apply: Xp | apply: ord_sup_sub]. set Z:= (fun_image _ f). have sFxoi: sub (fun_image X f) Z by apply: funI_S. have Zp: ordinal_set Z by apply:Os_funI => v /(ointvP oos) [uv _];apply: p1. apply: (oleA (ord_sup_M sFxoi Zp)). apply: ord_ub_sup => //. by apply: OS_sup; move=> i ifi; apply: Zp; apply: sFxoi. move=> i /funI_P [z /(ointvP oos) [uz zsX] ->]. move:(olt_sup p7 zsX) => [t tX zt]. apply:(oleT (proj1 (p2 _ _ uz zt ))). apply: ord_sup_ub => //; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)