proposition: Lemma derivable1P f x v : derivable f x v <-> derivable (fun h : R => f (h *: v + x)) 0 1.
proof: Proof. rewrite /derivable; set g1 := fun h => h^-1 *: _; set g2 := fun h => h^-1 *: _. suff -> : g1 = g2 by []. by rewrite funeqE /g1 /g2 => h /=; rewrite addr0 scale0r add0r [_%:A]mulr1. 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