proposition: Lemma strip_diag : forall f n, bisumsum_strip_diag' f n = bisumsum_strip_diag f n.
proof: Proof. intros. induction n. unfold bisumsum_strip_diag', bisumsum_strip_diag, bisumsum. simpl; ring. unfold bisumsum_strip_diag', bisumsum_strip_diag, bisumsum. rewrite bisumsum_one_step. rewrite bisum_one_step. unfold bisumsum_strip_diag', bisumsum_strip_diag, bisumsum in IHn. rewrite IHn. rewrite (bisum_one_step (fun i : Z => f i i)). repeat rewrite bisum_one_step. destruct (Z.eq_dec (Z_of_nat (S n)) (Z_of_nat (S n))); [ | apply False_ind; lia]; clear e. destruct (Z.eq_dec (Z_of_nat (S n)) (- Z_of_nat (S n))); [ apply False_ind; inversion e | ]; clear n0. destruct (Z.eq_dec (- Z_of_nat (S n)) (Z_of_nat (S n))); [ apply False_ind; inversion e | ]; clear n0. destruct (Z.eq_dec (- Z_of_nat (S n)) (- Z_of_nat (S n))); [ | apply False_ind; lia]; clear e. ring_simplify. assert (H : forall BII FNP FPN A B C D BIJ BIJS BPJS BNJS, BIJ + A + B + C + D = BIJS + BPJS + BNJS -> BIJ - BII + A + B + C + FNP + D + FPN = - BII + FNP + FPN + BIJS + BPJS + BNJS) by (intros; assert (H' : BIJ = - (A + B + C + D) + (BIJS + BPJS + BNJS)) by (rewrite <- H; ring); rewrite H'; ring). erewrite H; [reflexivity | ]. replace (bisum (fun j : Z => if Z.eq_dec (Z_of_nat (S n)) j then 0 else f (Z_of_nat (S n)) j) n) with (bisum_strip' (f (Z_of_nat (S n))) (Z_of_nat (S n)) n) by apply bisum_eq_sym. replace (bisum (fun j : Z => if Z.eq_dec (- Z_of_nat (S n)) j then 0 else f (- Z_of_nat (S n))%Z j) n) with (bisum_strip' (f (- Z_of_nat (S n)))%Z (- Z_of_nat (S n)) n)%Z by apply bisum_eq_sym. replace (bisum (fun i : Z => if Z.eq_dec i (- Z_of_nat (S n)) then 0 else f i (- Z_of_nat (S n))%Z) n) with (bisum_strip' (fun i => f i (- Z_of_nat (S n)))%Z (- Z_of_nat (S n)) n)%Z by trivial. replace (bisum (fun i : Z => if Z.eq_dec i (Z_of_nat (S n)) then 0 else f i (Z_of_nat (S n))) n) with (bisum_strip' (fun i => f i (Z_of_nat (S n)))%Z (Z_of_nat (S n)) n)%Z by trivial. repeat rewrite bisum_strip_nothing; [ | left | right | left | right ]; trivial. rewrite bisumsum_one_step. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith