proposition: Lemma derivable_pt_lim_scal_right : forall f x l a, derivable_pt_lim f x l -> derivable_pt_lim (fun y => f y * a) x (l * a).
proof: Proof. intros f x l a df; apply (derivable_pt_lim_ext (fun y => a * f y)). - intros z; rewrite Rmult_comm; reflexivity. - unfold Rdiv; rewrite Rmult_comm; apply derivable_pt_lim_scal; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv