proposition: Lemma mulo_numClosedFieldType (F : filter_on pT) (h1 h2 f g : pT -> R^o) : [o_F h1 of f] * [o_F h2 of g] =o_F (h1 * h2).
proof: Proof. rewrite [in RHS]littleoE // => _/posnumP[e]; near=> x. rewrite [`|_|]normrM -(sqrCK (ge0 e)) expr2 sqrtCM ?qualifE//=. rewrite (@normrM _ (h1 x) (h2 x)) mulrACA ler_pM //; near: x; by have [/= h] := littleo; apply. 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