proposition: Lemma sum_fixed_xif_zero: forall v k b (x: X A B), v < k -> b v = true -> sum 0 k (fun u => xif (b u) x 0) == x.
proof: Proof. intros v k b x ? H. apply leq_antisym. apply sum_leq. intros. case b. apply leq_refl. apply zero_inf. apply leq_sum. exists v. rewrite H. auto with arith. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)