Rational Cube Sum

Let $n$ be a non-negative rational number such that there are rational $x$ and $y$ with $x^3 + y ^ 3 = n$. Show that there are non-negative rational $a$ and $b$ such that $a ^ 3 + b ^ 3 = n$.

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Rat.Init

theorem solution (n : ℚ) (h1 : n ≥ 0) (h2 : ∃ x y, x ^ 3 + y ^ 3 = n) :
    ∃ a b : NNRat, a ^ 3 + b ^ 3 = n := sorry

Login to submit a solution.