proposition: Lemma scaleolx (K : numFieldType) (V W : normedModType K) {T : Type} (F : filter_on T) (a : W) (k : T -> K^o) (e : T -> V) (x : T) : ([o_F e of k] x) *: a = [o_F e of (fun y => [o_F e of k] y *: a)] x.
proof: Proof. rewrite [in RHS]littleoE //. have [->|a0] := eqVneq a 0. by move=> ??; apply: filterE => ?; rewrite scaler0 normr0 pmulr_rge0. move=> _/posnumP[eps]. have ea : 0 < eps%:num / `| a | by rewrite divr_gt0 // normr_gt0. have [g /(_ _ ea) ?] := littleo; near=> y. rewrite normrZ -ler_pdivlMr; first by rewrite mulrAC; near: y. by rewrite lt_def normr_eq0 a0 normr_ge0. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule