proposition: Fact dadd (f g : V -> W) x : differentiable f x -> differentiable g x -> continuous ('d f x \+ 'd g x) /\ (f + g) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ (0 : V) id.
proof: Proof. move=> df dg; split => [?|]; do ?exact: continuousD. apply/(@eqaddoE R); rewrite funeqE => y /=; rewrite -[(f + g) _]/(_ + _). by rewrite ![_ (_ + x)]diff_locallyx// addrACA addox addrACA. 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