proposition: Lemma card_null : forall (d : data) (q : queue), ~ In_queue d q -> card d q = 0%Z.
proof: Proof. simple induction q; simpl in |- *; intros. trivial. case (eq_data_dec d d0); intro. absurd (d = d0). red in |- *; intro; elim H0; auto. trivial. apply H; red in |- *; intro; elim H0; auto. Qed.
imports: bibli