inc(X, succ(X)). % you don't have to understand this.