proposition: Lemma count_inc_and_dec_alt_queue : forall q : queue Message, alternate q -> (reduce Message dec_count q + 1 >= reduce Message new_inc_count q)%Z.
proof: Proof. intros. intros. generalize (count_alt_queue q H); intro. decompose [and] H0. auto. Qed.
imports: DistributedReferenceCounting.machine4.alternate DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4