proposition: Lemma Derive_scal : forall f k x, Derive (fun x => k * f x) x = k * Derive f x.
proof: Proof. intros f k x. unfold Derive, Lim. have H : (forall x, k * Rbar.real x = Rbar.real (Rbar.Rbar_mult (Rbar.Finite k) x)). case: (Req_dec k 0) => [-> | Hk]. case => [l | | ] //= ; rewrite Rmult_0_l. case: Rle_dec (Rle_refl 0) => //= H _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => //= _ _. case: Rle_dec (Rle_refl 0) => //= H _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => //= _ _. case => [l | | ] //= ; rewrite Rmult_0_r. case: Rle_dec => //= H. case: Rle_lt_or_eq_dec => //=. case: Rle_dec => //= H. case: Rle_lt_or_eq_dec => //=. rewrite H. rewrite -Lim_seq_scal_l. apply f_equal, Lim_seq_ext => n. rewrite -Rmult_assoc. apply (f_equal (fun v => v / _)). ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv