proposition: Lemma bisumsum_strip_diag'_eq_but_diag_compat : forall f g n, (forall i j, i <> j -> f i j = g i j) -> bisumsum_strip_diag' f n = bisumsum_strip_diag' g n.
proof: Proof. intros. apply bisum_eq_compat; intros. apply bisum_eq_compat; intros. destruct (Z.eq_dec z z0). trivial. apply (H _ _ n0). Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith