proposition: Lemma reduce_append_nil2_symmetric : forall (q1 : queue E) (d : E), reduce q1 = (reduce (append E q1 (input E d (empty E))) - f d)%Z.
proof: Proof. intros q1 d. rewrite (reduce_append_nil2 q1 d). omega. Qed.
imports: Bool fifo