proposition: Lemma bisumsum_strip_diag'_switch_index : forall f n, bisumsum_strip_diag' (fun i j => f j i) n = bisumsum_strip_diag' f n.
proof: Proof. intros. unfold bisumsum_strip_diag'. rewrite bisumsum_switch_index. apply bisumsum_eq_compat; intros. destruct (Z.eq_dec y x); destruct (Z.eq_dec x y); try trivial; subst; apply False_ind; apply n0; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith