proposition: Lemma reduce_append : forall (q1 : queue E) (d : E) (q2 : queue E), reduce (append E q1 (input E d q2)) = (reduce (append E q1 q2) + f d)%Z.
proof: Proof. intro q1. elim q1. intros d q2. rewrite append_nil1. auto. intros d q H d0 q2. rewrite <- input_append. simpl in |- *. rewrite H. omega. Qed.
imports: Bool fifo