proposition: Lemma diff_locally_converse_part1 (f : R -> R) (a b x : R) : f \o shift x = cst a + b *: idfun +o_ (0 : R) id -> f x = a.
proof: Proof. rewrite funeqE => /(_ 0) /=; rewrite add0r => ->. by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0. 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