proposition: Lemma sum_zero i k (f: nat -> X A B): (forall n, n<k -> f (i+n)%nat == 0) -> sum i k f == 0.
proof: Proof. induction k; intro E; simpl_sum_r. reflexivity. rewrite IHk, E by auto with arith. apply plus_idem. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)