proposition: Lemma bisum_in : forall f g j n, (- Z_of_nat n <= j <= Z_of_nat n)%Z -> bisum (fun i : Z => if Z.eq_dec i j then g j else f i) n = bisum f n - f j + g j.
proof: Proof. intros. induction n. assert (j = Z0) by (replace (Z_of_nat O) with Z0 in H by trivial; lia); subst; trivial. simpl; ring. set (h := fun i => if Z.eq_dec i j then g j else f i). simpl bisum; unfold h in *. destruct (Z.eq_dec (Zpos (P_of_succ_nat n)) j) as [e|e]; destruct (Z.eq_dec (Zneg (P_of_succ_nat n)) j) as [e'|e']; subst; try inversion e'. rewrite bisum_not_in. ring. right; destruct n; simpl. lia. apply Psucc_lt. rewrite bisum_not_in. ring. left; destruct n; simpl. lia. apply Psucc_lt_neg. rewrite IHn. ring. split; rewrite inj_S in H. destruct (Z_le_gt_dec (- Z_of_nat n) j); trivial. replace (Zneg (P_of_succ_nat n)) with (- Z_of_nat (S n))%Z in e' by trivial. rewrite inj_S in *. lia. destruct (Z_le_gt_dec j (Z_of_nat n)); trivial. replace (Zpos (P_of_succ_nat n)) with (Z_of_nat (S n))%Z in e by trivial. rewrite inj_S in *. lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith