proposition: Lemma derivable_pt_lim_cst c x : derivable_pt_lim (fun _ : R => c) x 0.
proof: Proof. rewrite /derivable_pt_lim => e e0. exists (mkposreal _ e0) => h h0 Hh; by rewrite subRR subR0 div0R normR0. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext