proposition: Lemma scale_littleo_subproof (F : filter_on T) e (df : {o_F e}) a : littleo_def F (a *: (df : _ -> _)) e.
proof: Proof. have [->|a0] := eqVneq a 0; first by rewrite scale0r. move=> _ /posnumP[eps]; have aa := normr_eq0 a; near=> x => /=. rewrite normrZ -ler_pdivlMl ?lt_def ?aa ?a0 //= mulrA; near: x. by apply: littleoP; rewrite mulr_gt0 // invr_gt0 ?lt_def ?aa ?a0 /=. 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