proposition: Lemma rooted_positive_or_null : forall (s0 x y : Site) (q : queue Message), (rooted s0 x y q >= 0)%Z.
proof: Proof. intros. unfold rooted in |- *. apply reduce_positive_or_null. intro. apply rooted_fun_positive_or_null. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm