proposition: Lemma ofs_mul_restr a y (c:= card_max a y) (E := cnext c) (f:= Lf (fun z => a *o z) E E) : \0o <o a -> ordinalp y -> [/\ (forall x, inc x E -> inc (a *o x) E ), (forall x, x <=o y -> inc x E), normal_function f E E & forall x, inc x E -> Vf f x = a *o x].
proof: Proof. move => ap oy. have oa:= (proj32_1 ap). move: (omax_p3 oa oy); rewrite -/(card_max _ _) -/c -/E. move => [icc ae ye]. have pa: forall x, x <=o y -> inc x E. have oc:=(proj1 (CS_cnext (proj1 icc))). have yc:y <o cnext c by apply/(oltP oc). move => x xe; apply/(oltP oc); apply: (ole_ltT xe yc). have pb: forall x, inc x E -> inc (a *o x) E. by move => x xe;apply: cnext_prod. have pc:= (normal_ofs_restriction icc (oprod_normal ap) pb). by split => //x xe; rewrite /f LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)