proposition: Lemma sum_cut k' i k (f: nat -> X A B): sum i (k'+k) f == sum i k f + sum (k+i) k' f.
proof: Proof. induction k'; simpl_sum_r. auto with algebra. rewrite IHk', plus_assoc. auto with compat lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)