proposition: Lemma reduce_positive : forall q : queue E, (reduce q >= 0)%Z.
proof: Proof. intros q. elim q. simpl in |- *. omega. intros d q0 H. simpl in |- *. apply sum_positive. auto. exact (positive_function d). Qed.
imports: Bool fifo