proposition: Lemma Z_nat_business : forall x y : positive, nat_of_P y < nat_of_P x -> (Zpos y < Zpos x)%Z.
proof: Proof. intros. unfold Zlt in |- *. unfold Zcompare in |- *. apply nat_of_P_lt_Lt_compare_complement_morphism. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8