tff(goal, conjecture,
    ![X: $int] : (
        $greater(X, 1) => $greater($product(X, X), X)
    )
).