proposition: Lemma ofs_add_restr a y (c:= card_max a y) (E := cnext c) (f:= Lf (fun z => a +o z) E E) : ordinalp 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 => oa oy. 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_sum. move: (normal_ofs_restriction icc (osum_normal oa) pb) => pc. by split => //x xe; rewrite /f LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)