proposition: Lemma diff_post_card_mess : forall (m m' : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message), m <> m' \/ s1 <> s3 \/ s2 <> s4 -> card_mess m (Post_message m' b s3 s4 s1 s2) = card_mess m (b s1 s2).
proof: Proof. intros; unfold card_mess in |- *; elim H; intros. case (eq_queue_dec s1 s3 s2 s4); intro. decompose [and] a; rewrite H1; rewrite H2; rewrite post_here; apply input_diff_card; trivial. rewrite post_elsewhere; elim o; auto. rewrite post_elsewhere; elim H0; auto. Qed.
imports: counting