proposition: Lemma bisumsum_switch_index : forall f n, bisumsum (fun i j => f j i) n = bisumsum f n.
proof: Proof. intros. induction n. trivial. unfold bisumsum in *. rewrite bisumsum_one_step. rewrite bisumsum_one_step. simpl. rewrite IHn. replace (bisum (f (Zneg (P_of_succ_nat n))) n) with (bisum (fun i => f (Zneg (P_of_succ_nat n)) i) n) by (apply bisum_eq_compat; trivial). replace (bisum (f (Zpos (P_of_succ_nat n))) n) with (bisum (fun i => f (Zpos (P_of_succ_nat n)) i) n) by (apply bisum_eq_compat; trivial). ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith