proposition: Lemma sum_leq (f : nat -> X A B) i k x: (forall n, i <= n -> n < i +k -> f n <== x) -> sum i k f <== x.
proof: Proof. revert x. induction k. intros x H. simpl_sum_r. apply plus_neutral_left. intros x H. simpl_sum_r. rewrite (IHk x) , H. auto using plus_destruct_leq. auto with arith. auto with arith. intros; apply H; lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)