proposition: Lemma not_in_q_shuffle1 : forall (m1 m2 : data) (q3 q4 : queue data), ~ In_queue data m2 (input data m1 (append data q3 q4)) -> ~ In_queue data m2 (append data q3 (input data m1 q4)).
proof: Proof. intros m1 m2 q3 q4 H. apply not_inqueue_append. simpl in |- *. split. unfold not in |- *; intro. elim H. simpl in |- *. right. apply inqueue_append. auto. unfold not in |- *; intro. elim H. simpl in |- *. elim H0; intro. auto. right. apply inqueue_append. auto. Qed.
imports: bibli