proposition: Lemma sum_plus : forall (f : nat -> X A B) i k a, 0 < k -> sum i k f + a == sum i k (fun n => f n + a).
proof: Proof. induction k; intros. lia_false. simpl_sum_r. destruct (eq_nat_dec 0 k). subst. simpl_sum_r. auto with algebra. setoid_rewrite <- IHk. setoid_rewrite switch at 2. rewrite <- !plus_assoc, plus_idem. reflexivity. lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)