proposition: Remark add_reduce : forall x y a u w z : Z, (y - a)%Z = (z + w - u)%Z -> (x + y - a)%Z = (x + z + w - u)%Z.
proof: Proof. intros; omega. Qed.
imports: DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3