proposition: Lemma collect_card_mess : forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), first Message (b s1 s2) = value Message m -> card_mess m (Collect_message b s1 s2 s1 s2) = (card_mess m (b s1 s2) - 1)%Z.
proof: Proof. intros; unfold card_mess in |- *; rewrite collect_here; apply firstout_pred_card; trivial. Qed.
imports: counting