proposition: Lemma compOo_eqox (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') : forall x, [O_ (0 : V') id of g] ([o_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
proof: Proof. by move=> x; rewrite -[LHS]/((_ \o _) x) compOo_eqo. 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