Theorem: Primitive of x squared by Root of a squared minus x squared

:$\ds \int x^2 \sqrt {a^2 - x^2} \rd x = -\frac {x \paren {\sqrt {a^2 - x^2} }^3} 4 + \frac {a^2 x \sqrt {a^2 - x^2} } 8 + \frac {a^4} 8 \arcsin \frac x a + C$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = x^2
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int x^2 \sqrt {a^2 - x^2} \rd x
      | r = \int \frac {z \sqrt {a^2 - z} \rd z} {2 \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \sqrt {z \paren {a^2 - z} } \rd z
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
Recall:
{{begin-eqn}}
{{eqn | l = \int \sqrt {\paren {a x + b} \paren {p x + q} } \rd x
      | r = \frac {2 a p x + b p + a q} {4 a p} \sqrt {\paren {a x + b} \paren {p x + q} } - \frac {\paren {b p - a q}^2} {8 a p} \int \frac {\d x} {\sqrt {\paren {a x + b} \paren {p x + q} } }
      | c = Primitive of $\sqrt {\paren {a x + b} \paren {p x + q} }$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \frac {2 a p x + b p + a q} {4 a p}
      | r = \frac {2 \times 1 \times \paren {-1} z + 0 \times \paren {-1} + 1 \times a^2} {4 \times 1 \times \paren {-1} }
      | c = setting $a \gets 1$, $b \gets 0$, $p \gets -1$, $q \gets a^2$, $x \gets z$
}}
{{eqn | r = \frac {-2 z + a^2} {-4}
      | c = simplifying
}}
{{eqn | n = 1
      | r = \frac {2 z - a^2} 4
      | c = simplifying further
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \frac 1 2 \int \sqrt {z \paren {a^2 - z} } \rd z
      | r = \frac 1 2 \paren {\frac {2 z - a^2} 4 \sqrt {z \paren {a^2 - z} } - \frac {\paren {0 \times \paren {-1} + 1 \times a^2}^2} {8 \times 1 \times \paren {-1} } \int \frac {\d z} {\sqrt {z \paren {a^2 - z} } } }
      | c = setting $a \gets 1$, $b \gets 0$, $p \gets -1$, $q \gets a^2$, $x \gets z$
}}
{{eqn | r = \frac {2 z - a^2} 8 \sqrt {z \paren {a^2 - z} } + \frac {a^4} {16} \int \frac {\d z} {\sqrt {z \paren {a^2 - z} } }
      | c = simplifying
}}
{{end-eqn}}
Recall:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {\paren {a x + b} \paren {p x + q} } }
      | r = \dfrac {-1} {\sqrt {-a p} } \map \arcsin {\dfrac {2 a p x + b p + a q} {a q - b p} } + C
      | c = Primitive of $\dfrac 1 {\sqrt {\paren {a x + b} \paren {p x + q} } }$ for $a > 0, p < 0$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \frac {2 z - a^2} 8 \sqrt {z \paren {a^2 - z} } + \frac {a^4} {16} \int \frac {\d z} {\sqrt {z \paren {a^2 - z} } }
      | r = \frac {2 z - a^2} 8 \sqrt {z \paren {a^2 - z} } + \frac {a^4} {16} \paren {\dfrac {-1} {\sqrt {-1 \times \paren {-1} } } \arcsin \frac {2 z - a^2} 4} + C
      | c = from $(1)$, and $a \gets 1$, $b \gets 0$, $p \gets -1$, $q \gets a^2$, $x \gets z$
}}
{{eqn | r = \frac {2 z - a^2} 8 \sqrt {z \paren {a^2 - z} } + \frac {a^4} {16} \paren {-\arcsin \frac {2 z - a^2} 4} + C
      | c = simplifying
}}
{{eqn | r = \frac {2 x^2 - a^2} 8 \sqrt {x^2 \paren {a^2 - x^2} } + \frac {a^4} {16} \paren {-\arcsin \frac {2 x^2 - a^2} 4} + C
      | c = substituting $x^2$ back for $z$
}}
{{eqn | r = \frac {2 x^2 - 2 a^2 + a^2} 8 \sqrt {x^2 \paren {a^2 - x^2} } + \frac {a^4} {16} \paren {-\arcsin \frac {2 x^2 - a^2} 4} + C
      | c = 
}}
{{eqn | r = -\frac {a^2 - x^2} 4 x \sqrt {a^2 - x^2} + \frac {a^2 x \sqrt {a^2 - x^2} } 8 + \frac {a^4} {16} \paren {-\arcsin \frac {2 x^2 - a^2} 4} + C
      | c = rearranging
}}
{{eqn | r = -\frac {x \paren {\sqrt {a^2 - x^2} }^3} 4 + \frac {a^2 x \sqrt {a^2 - x^2} } 8 + \frac {a^4} {16} \paren {-\arcsin \frac {2 x^2 - a^2} 4} + C
      | c = simplifying
}}
{{end-eqn}}
{{finish|Can this proof be salvaged?}}