proposition: Lemma oprod_normal a: \0o <o a -> normal_ofs (fun z => a *o z).
proof: Proof. move=> ap; split; first by move=> x y xy; apply: oprod_Meqlt. have oa:= proj32_1 ap. move=> b lb; move: (lb) => [ob iob olbp]. have op:= OS_prod2 oa ob. have osE: ordinal_set (fun_image b (oprod2 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 ->]. by move: (proj1 (oprod_Meqlt xx ap)). split; [exact | by apply:OS_sup | move => w ]. rewrite (oprod_rec_def oa ob) => /funI_P [z /setX_P [z1 z2 z3] ->]. have z4:= (olbp _ z3). have o3 := (Os_ordinal ob z3). have o4:= (Os_ordinal ob z4). apply /setU_P; exists (a *o (osucc (Q z))). apply /(oltP (OS_prod2 oa o4)); rewrite (oprod2_succ oa o3). by apply: (osum_Meqlt _ (OS_prod2 oa o3)); apply/(oltP oa). apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)