proposition: Lemma not_in_q_output : forall (data : Set) (d : data) (q : queue data), ~ In_queue data d q -> ~ In_queue data d (first_out data q).
proof: Proof. simple induction q. simpl in |- *; trivial. intros d0 q0; case q0; simpl in |- *; intros. trivial. intuition. intuition. Qed.
imports: bibli