proposition: Lemma decomp_sum : forall {R : ConstructiveReals} (An:nat -> CRcarrier R) (N:nat), (0 < N)%nat -> CRsum An N == An 0%nat + CRsum (fun i:nat => An (S i)) (pred N).
proof: Proof. induction N. - intros. exfalso. inversion H. - intros _. destruct N. + simpl. reflexivity. + simpl. rewrite IHN. * rewrite CRplus_assoc. apply CRplus_morph. -- reflexivity. -- reflexivity. * apply le_n_S, Nat.le_0_l. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits