proposition: Lemma reduce_first_out : forall (q : queue data) (m : data), first data q = value data m -> reduce data f (first_out data q) = (reduce data f q - f m)%Z.
proof: Proof. intros q m H. rewrite (reduce_append_nil2_symmetric data f (first_out data q) m). rewrite (append_first_out2 data m q). auto. auto. Qed.
imports: Bool fifo