proposition: Lemma compare_sum_xif_zero: forall k k' b c (x: X A B), (forall i, i < k -> b i = true -> exists2 j, j < k' & c j = true) -> sum 0 k (fun i => xif (b i) x 0) <== sum 0 k' (fun j => xif (c j) x 0).
proof: Proof. intros until x; intro H. apply sum_leq. intros n _ Hn. specialize (H _ Hn). destruct (b n). destruct (H refl_equal) as [j ? Hj]. apply leq_sum. exists j. rewrite Hj. auto with arith. apply zero_inf. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)