proposition: Lemma bisumsum_strip_diag'_plus : forall f g n, bisumsum_strip_diag' (fun i j => f i j + g i j) n = bisumsum_strip_diag' f n + bisumsum_strip_diag' g n.
proof: Proof. intros. unfold bisumsum_strip_diag'. unfold bisumsum. rewrite <- bisum_plus. apply bisum_eq_compat; intros. unfold zr2. rewrite <- bisum_plus. apply bisum_eq_compat; intros. unfold zr2. destruct (Z.eq_dec z z0); ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith