proposition: Lemma 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. elim H; intro. contradiction. auto. simpl in |- *. intros d q H q2 H0. elim H0; intro. elim H1; intro. auto. right. apply H. auto. right. apply H. auto. Qed.
imports: bibli