proposition: Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\ cst a \o shift x = cst (cst a x) + \0 +o_ (0 : V) id.
proof: Proof. split; first exact: cst_continuous. apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _). by rewrite littleoE; last exact: littleo0_subproof. 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