proposition: Lemma append_assoc : forall q1 q2 q3 : queue data, append q1 (append q2 q3) = append (append q1 q2) q3.
proof: Proof. intro q1. elim q1. intros q2 q3. rewrite append_nil1. rewrite append_nil1. auto. intros d q H q2 q3. simpl in |- *. rewrite H. auto. Qed.
imports: bibli