proposition: Lemma bisumsum_plus_switch : forall f g n, bisumsum_strip_diag' (fun i j => f i j + g i j) n = bisumsum_strip_diag' (fun i j => f i j + g j i) n.
proof: Proof. intros. rewrite bisumsum_strip_diag'_plus. rewrite <- bisumsum_strip_diag'_switch_index with g n. rewrite <- bisumsum_strip_diag'_plus. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith