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 [RHS]bigOE//; have [ O1 k1 Oh1] := bigO; have [ O2 k2 Oh2] := bigO. near=> k; move: Oh1 Oh2; apply: filter_app2; near=> x => leOh1 leOh2. rewrite [`|_|]normrM (le_trans (ler_pM _ _ leOh1 leOh2)) //. by rewrite mulrACA [`|_| in leRHS]normrM ler_wpM2r // ?mulr_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