proposition: Lemma eqo_pair (U V' W' : normedModType R) (F : filter_on U) (f : U -> V') (g : U -> W') : (fun t => ([o_F id of f] t, [o_F id of g] t)) =o_F id.
proof: Proof. apply/eqoP => _/posnumP[e]; near=> x; rewrite num_le_maxl /=. by apply/andP; split; near: x; apply: littleoP. Unshelve. all: by end_near. 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