proposition: Lemma sum_incr (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 2 sum_enter_right. rewrite IHk, E by auto with arith. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)