proposition: Lemma sum_enter_right i k (f: nat -> X A B): sum i (S k) f == sum i k f + f (i+k)%nat.
proof: Proof. revert i; induction k; intro i. simpl. rewrite Nat.add_0_r; apply plus_com. change (sum i (S (S k)) f) with (f i + sum (S i) (S k) f). rewrite IHk, plus_assoc. simpl. auto with compat. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)