proposition: Lemma le_xi_yi : forall s0 : Site, (xi c0 s0 >= yi c0 s0)%Z.
proof: Proof. intros; unfold xi, yi, ctrl_copy, ctrl_dec, ctrl_inc in |- *. generalize (pos_card_mess copy (bm c0 owner s0)); intros. generalize (legal_alternate s0 c0 Hlegal); intros. case (eq_bool_dec (rt c0 s0)); intro; rewrite e; unfold Int in |- *. generalize (alt_dec_inc (bm c0 s0 owner) H0); omega. generalize (legal_false_D c0 s0 Hlegal e); intro. generalize (D_dec_inc (bm c0 s0 owner) H0 H1); omega. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc