proposition: Lemma splitSum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (filter : nat -> bool) (n : nat), CRsum un n == CRsum (fun i => if filter i then un i else 0) n + CRsum (fun i => if filter i then 0 else un i) n.
proof: Proof. induction n. - simpl. destruct (filter O). + symmetry; apply CRplus_0_r. + symmetry. apply CRplus_0_l. - simpl. rewrite IHn. clear IHn. destruct (filter (S n)). + do 2 rewrite CRplus_assoc. apply CRplus_morph. * reflexivity. * rewrite CRplus_comm. apply CRplus_morph. -- reflexivity. -- rewrite CRplus_0_r. reflexivity. + rewrite CRplus_0_r. rewrite CRplus_assoc. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits