proposition: Lemma CRsum_eq : forall {R : ConstructiveReals} (An Bn:nat -> CRcarrier R) (N:nat), (forall i:nat, (i <= N)%nat -> An i == Bn i) -> CRsum An N == CRsum Bn N.
proof: Proof. induction N. - intros. exact (H O (Nat.le_refl _)). - intros. simpl. apply CRplus_morph. + apply IHN. intros. apply H. apply (Nat.le_trans _ N _ H0), le_S, Nat.le_refl. + apply H, Nat.le_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits