proposition: Lemma leq_sum (f: nat -> X A B) i k x: (exists n, i<=n /\ n<i+k /\ x <== f n) -> x <== sum i k f.
proof: Proof. intros [n [? [? E]]]. rewrite E, (sum_cut_nth (n-i)) by lia. replace (i+(n-i))%nat with n by auto with arith. rewrite <- plus_make_left. apply plus_make_right. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)