proposition: Lemma not_inqueue_append : forall (m : data) (q1 q2 : queue data), ~ In_queue data m q1 /\ ~ In_queue data m q2 -> ~ In_queue data m (append data q1 q2).
proof: Proof. intros m q1. elim q1. simpl in |- *. intros q2 H. decompose [and] H; auto. simpl in |- *; intros. decompose [and] H0. unfold not in |- *. intro H1'. elim H1'; intro. elim H1. auto. unfold not in H. apply (H q2). split. intro H5. elim H1. auto. intro; elim H2; auto. auto. Qed.
imports: bibli