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