proposition: Lemma osum_normal a: ordinalp a -> normal_ofs (fun z => a +o z).
proof: Proof. move=> oa; split; first by move=> x y xy; apply: osum_Meqlt. move=> b lb; move: (lb) => [ob iob olbp]. have op:= OS_sum2 oa ob. have osE: ordinal_set (fun_image b (osum2 a)). apply: Os_funI => c /(Os_ordinal ob) oc; fprops. apply:oleA; last first. apply:ord_ub_sup => // x /funI_P [z /(oltP ob) xx ->]. exact: (proj1 (osum_Meqlt xx oa)). split; [exact | by apply:OS_sup | move => w]. rewrite (osum_rec_def oa ob) => h; apply /setU_P. case /setU2_P:h. by move => wa; exists a => //; apply /funI_P;ex_tac; rewrite osum0r. move /funI_P => [z za zb]; exists (osucc w); fprops. have oz := (Os_ordinal ob za). by apply /funI_P; exists (osucc z); [apply: olbp | rewrite zb - osum2_succ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)