proposition: Lemma sum_eq_R0 : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat), (forall k:nat, un k == 0) -> CRsum un n == 0.
proof: Proof. induction n. - intros. apply H. - intros. simpl. rewrite IHn. + rewrite H. apply CRplus_0_l. + exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits