proposition: Lemma bisum_eq_sym : forall f z n, bisum (fun i : Z => if Z.eq_dec i z then 0 else f z i) n = bisum (fun j : Z => if Z.eq_dec z j then 0 else f z j) n.
proof: Proof. intros; apply bisum_eq_compat; intros. destruct (Z.eq_dec z0 z); destruct (Z.eq_dec z z0); try trivial; subst; apply False_ind; apply n0; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith