proposition: Lemma Csigma_split : forall (f : nat -> C) (low high k : nat), (low <= k)%nat -> (k < high)%nat -> Csigma f low high = (Csigma f low k + Csigma f (S k) high).
proof: Proof. intros f low high k l_le_k k_lt_h. unfold Csigma. apply (proj1 (Ceq _ _)) ; split. rewrite <- Cre_add_compat ; do 3 rewrite <- sum_f_C0_Cre_compat. assert (H := sigma_split (fun n => Cre (f n)) l_le_k k_lt_h) ; unfold sigma in H ; assumption. rewrite <- Cim_add_compat ; do 3 rewrite <- sum_f_C0_Cim_compat. assert (H := sigma_split (fun n => Cim (f n)) l_le_k k_lt_h) ; unfold sigma in H ; assumption. Qed.
imports: Rsequence_def Rinterval Ranalysis_def Rsequence_cv_facts Rsequence_tactics MyRIneq Cfunctions Csequence Csequence_facts CFsequence Cnorm Cprop_base Ctacfield Lia Lra PeanoNat Cmet Canalysis_def Canalysis_deriv