proposition: Lemma append_right_non_empty : forall (q1 q2 : queue data) (d : data), append q1 (input data d q2) <> empty data.
proof: Proof. intros q1 q2 d. elim q1. simpl in |- *. discriminate. intros d0 q H. rewrite <- input_append. discriminate. Qed.
imports: bibli