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