proposition: Remark add_reduce19 : forall x1 x2 x3 y1 y2 y3 y4 : Z, x1 = y1 -> (y2 - y4 + (y3 + 1) < x2 + x3)%Z -> (y1 + (y2 - y4) + (y3 + 1) < x1 + x2 + x3)%Z.
proof: Proof. intros; omega. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8