proposition: Lemma reduce_in_queue_strictly_positive : forall (x : E) (q : queue E), (f x > 0)%Z -> In_queue E x q -> (reduce E f q > 0)%Z.
proof: Proof. simple induction q; simpl in |- *. intuition. intro d. case (eq_E_dec d x); intro. rewrite e; intros. generalize (reduce_positive_or_null E f positive_function q0); intro. clear H. omega. intros q0 H H0 H1. elim H1; intro. elim n; auto. generalize (positive_function d); intro. generalize (H H0 H2); intro. omega. Qed.
imports: Bool fifo