proposition: Lemma firstout_diff_card : forall (d : data) (q : queue data), first data q <> value data d -> card data eq_data_dec d (first_out data q) = card data eq_data_dec d q.
proof: Proof. simple induction q. auto. intros d0 q0; case q0. simpl in |- *; intros. rewrite case_ineq. trivial. red in |- *; intro; elim H0. rewrite H1; trivial. simpl in |- *; intros. rewrite H; auto. Qed.
imports: bibli