proposition: Lemma sum_scale : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R) (n : nat), CRsum (fun k : nat => u k * a) n == CRsum u n * a.
proof: Proof. induction n. - simpl. rewrite (Rmul_comm (CRisRing R)). reflexivity. - simpl. rewrite IHn. rewrite CRmult_plus_distr_r. apply CRplus_morph. + reflexivity. + rewrite (Rmul_comm (CRisRing R)). reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits