proposition: Lemma reduce_positive_or_null : forall q : queue E, (reduce E f q >= 0)%Z.
proof: Proof. intros q. elim q. simpl in |- *. omega. intros d q0 H. simpl in |- *. generalize (positive_function d). intro H0. omega. Qed.
imports: Bool fifo