proposition: Lemma firstout_pred_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 - 1)%Z.
proof: Proof. simple induction q. simpl in |- *; intros H; discriminate H. simpl in |- *; intros d0 q0; case q0. case (eq_data_dec d d0); intros. simpl in |- *; omega. injection H0; intros. absurd (d0 = d); auto. case (eq_data_dec d d0); intros. rewrite <- e; rewrite input_S_card. rewrite H. omega. trivial. trivial. rewrite input_diff_card. apply H; trivial. trivial. Qed.
imports: bibli