proposition: Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R) of f x]| = 0.
proof: Proof. rewrite /cst /=; have [e /(_ (`|e x|/2) _)/nbhs_singleton /=] := littleo. rewrite pmulr_lgt0 // [`|1|]normr1 mulr1 [leLHS]splitr gerDr pmulr_lle0 //. by move=> /implyP; case : real_ltgtP; rewrite ?realE ?normrE //= lexx. 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