proposition: Lemma strct_pos_card_mess : forall (m : Message) (q : queue Message), In_queue Message m q -> (card_mess m q > 0)%Z.
proof: Proof. intros; unfold card_mess in |- *; apply card_strct_pos; trivial. Qed.
imports: List fifo table