proposition: Lemma card_strct_pos : forall (d : data) (q : queue), In_queue d q -> (card d q > 0)%Z.
proof: Proof. simple induction q; simpl in |- *. contradiction. intros; case (eq_data_dec d d0); intro. generalize (card_pos d q0); omega. elim H0; intro. absurd (d = d0); trivial. auto. Qed.
imports: bibli