proposition: Lemma sum_cut_fun i k (f g: nat -> X A B): sum i k (fun u => f u + g u) == sum i k f + sum i k g.
proof: Proof. induction k; simpl_sum_r. auto with algebra. rewrite IHk. rewrite switch. setoid_rewrite plus_com at 6. rewrite 2plus_assoc. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)