proposition: Lemma littleo_center0 (x : V) (f : V -> W) (e : V -> V) : [o_x e of f] = [o_ (0 : V) (e \o shift x) of f \o shift x] \o center x.
proof: Proof. rewrite /the_littleo /insubd /=; have [g /= _ <-{f}|/asboolP Nfe] /= := insubP. rewrite insubT //= ?comp_shiftK //; apply/asboolP => _/posnumP[eps]. rewrite [\forall x \near _, _ <= _](near_shift x) sub0r; near=> y. by rewrite /= subrK; near: y; have /eqoP := littleo_eqo g; apply. rewrite insubF //; apply/asboolP => fe; apply: Nfe => _/posnumP[eps]. by rewrite [\forall x \near _, _ <= _](near_shift 0) subr0; apply: fe. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms