The blow-up of the plane at the origin is smooth

import Mathlib
import Definitions.Def_MaximalSeshadriConstants
import Definitions.Def_SeshadriPrelim6

namespace OAI

section
namespace MaximalSeshadri.PlaneBlowup
noncomputable section
open MvPolynomial ReesGrading
variable (K : Type) [Field K]

end

noncomputable section
open AlgebraicGeometry CategoryTheory MvPolynomial ReesGrading
variable (K : Type) [Field K]

theorem smooth_structureMap : SmoothOfRelativeDimension 2 (structureMap K) := by
  sorry

end
end MaximalSeshadri.PlaneBlowup
end
end OAI