proposition: Lemma sum_collapse n (f: nat -> X A B) i k: n<k -> (forall x, x <> (i+n)%nat -> f x == 0) -> sum i k f == f (i+n)%nat.
proof: Proof. intros Hn H. rewrite (sum_cut_nth n), 2 sum_zero by ( auto || intros; apply H ; lia). rewrite plus_neutral_left. apply plus_neutral_right. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)