proposition: Lemma normal_shift f a: normal_ofs f -> ordinalp a -> normal_ofs (fun z => (f(a +o z) -o a)).
proof: Proof. move => sa oa. have sb:= (normal_ofs_compose sa (osum_normal oa)). have sc:= (odiff_normal oa). set f1 := (odiff^~ a); set f2:= (f \o (osum2 a)). have h1: a <=o f2 \0o. rewrite /f2 /= (osum0r oa); exact: (osi_gex (proj1 sa) oa). move/normal_ofs_equiv1: sb => sb'; apply/normal_ofs_equiv1. exact:(normal_ofs_compose1 oa OS0 h1 sc sb'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)