proposition: Lemma disjoint_reduce : forall (f1 f2 : E -> Z) (q : queue E), reduce E (fun_sum f1 f2) q = (reduce E f1 q + reduce E f2 q)%Z.
proof: Proof. simple induction q. simpl in |- *. auto. intros d q0 H. simpl in |- *. rewrite H. unfold fun_sum in |- *. omega. Qed.
imports: Bool fifo