avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of x by Arccosine of x over a

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

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-1} {\sqrt {a^2 - x^2} }
      | c = Derivative of $\arccos \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^2} 2
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \arccos \frac x a \rd x
      | r = \frac {x^2} 2 \arccos \frac x a - \int \frac {x^2} 2 \paren {\frac {-1} {\sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^2} 2 \arccos \frac x a + \frac 1 2 \int \frac {x^2 \rd x} {\sqrt {a^2 - x^2} } + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^2} 2 \arccos \frac x a + \frac 1 2 \paren {\frac {-x \sqrt {a^2 - x^2} } 2 + \frac {a^2} 2 \arcsin \frac x a} + C
      | c = Primitive of $\dfrac {x^2} {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = \frac {x^2} 2 \arccos \frac x a - \frac {x \sqrt {a^2 - x^2} } 4 + \frac {a^2} 4 \paren {\frac \pi 2 - \arccos \frac x a} + C
      | c = Sum of Arcsine and Arccosine
}}
{{eqn | r = \paren {\frac {x^2} 2 - \frac {a^2} 4} \arccos \frac x a - \frac {x \sqrt {a^2 - x^2} } 4 + \frac {\pi a^2} 8 + C
      | c = simplifying
}}
{{eqn | r = \paren {\frac {x^2} 2 - \frac {a^2} 4} \arccos \frac x a - \frac {x \sqrt {a^2 - x^2} } 4 + C
      | c = subsuming $\dfrac {\pi a^2} 8$ into the arbitrary constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x squared by Arccosine of x over a

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

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-1} {\sqrt {a^2 - x^2} }
      | c = Derivative of $\arccos \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^3} 3
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^2 \arccos \frac x a \rd x
      | r = \frac {x^3} 3 \arccos \frac x a - \int \frac {x^3} 3 \paren {\frac {-1} {\sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^3} 3 \arccos \frac x a + \frac 1 3 \int \frac {x^3 \rd x} {\sqrt {a^2 - x^2} } + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^3} 3 \arccos \frac x a + \frac 1 3 \paren {\frac {\paren {\sqrt {a^2 - x^2} }^3} 3 - a^2 \sqrt {a^2 - x^2} } + C
      | c = Primitive of $\dfrac {x^3} {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = \frac {x^3} 3 \arccos \frac x a - \frac {\paren {x^2 + 2 a^2} \sqrt {a^2 - x^2} } 9 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccosine of x over a over x

:$\ds \int \dfrac 1 x \arccos \frac x a \rd x = \frac \pi 2 \ln \size x - \int \frac {\arcsin \frac x a \rd x} x + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac 1 x \arccos \frac x a \rd x
      | r = \int \dfrac 1 x \paren {\frac \pi 2 - \arcsin \frac x a} \rd x
      | c = Sum of Arcsine and Arccosine
}}
{{eqn | r = \frac \pi 2 \int \frac {\d x} x - \int \dfrac 1 x \arcsin \frac x a \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac \pi 2 \ln \size x - \int \dfrac 1 x \arcsin \frac x a \rd x + C
      | c = Primitive of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccosine of x over a over x squared

:$\ds \int \frac 1 {x^2} \arccos \frac x a \rd x  = -\frac 1 x \arccos \frac x a + \frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } x} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-1} {\sqrt {a^2 - x^2} }
      | c = Derivative of $\arccos \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-1} x
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac 1 {x^2} \arccos \frac x a \rd x
      | r = \arccos \frac x a \paren {\frac {-1} x} - \int \paren {\frac {-1} x} \paren {\frac {-1} {\sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = -\frac 1 x \arccos \frac x a - \int \frac {\d x} {x \sqrt {a^2 - x^2} } \rd x + C
      | c = simplifying
}}
{{eqn | r = -\frac 1 x \arccos \frac x a + \frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } + C
      | c = Primitive of $\dfrac 1 {x \sqrt {a^2 - x^2} }$
}}
{{eqn | r = -\frac 1 x \arccos \frac x a + \frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } x} + C
      | c = Domain of Real Arccosine is Non-Negative
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Arccosine of x over a

:$\ds \int \paren {\arccos \frac x a}^2 \rd x = x \paren {\arccos \frac x a}^2 - 2 x - 2 \sqrt {a^2 - x^2} \arccos \frac x a + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cos u 
      | r = \frac x a
      | c = {{Defof|Real Arccosine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sin u 
      | r = \sqrt {1 - \frac {x^2} {a^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \paren {\arccos \frac x a}^2 \rd x
      | r = -a \int u^2 \sin u \rd x
      | c = Primitive of Function of Arccosine
}}
{{eqn | r = -a \paren {2 u \sin u + \paren {2 - u^2} \cos u} + C
      | c = Primitive of $x^2 \sin a x$ where $a = 1$
}}
{{eqn | r = -a \paren {2 \arccos \frac x a \sqrt {1 - \frac {x^2} {a^2} } + \paren {2 - \paren {\arccos \frac x a}^2} \frac x a} + C
      | c = substituting for $u$, $\sin u$ and $\cos u$
}}
{{eqn | r = x \paren {\arccos \frac x a}^2 - 2 x - 2 \sqrt {a^2 - x^2} \arccos \frac x a + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arctangent of x over a

:$\ds \int \arctan \frac x a \rd x = x \arctan \frac x a - \frac a 2 \map \ln {x^2 + a^2} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \tan u 
      | r = \frac x a
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sec u 
      | r = \sqrt {1 + \frac {x^2} {a^2} }
      | c = Difference of Squares of Secant and Tangent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arctan \frac x a \rd x
      | r = a \int u \sec^2 u \rd u
      | c = Primitive of Function of Arctangent
}}
{{eqn | r = a \paren {u \tan u + \ln \size {\cos u} } + C
      | c = Primitive of $x \sec^2 a x$ with $a = 1$
}}
{{eqn | r = a u \tan u - a \ln \size {\sec u} + C
      | c = Logarithm of Reciprocal and Secant is Reciprocal of Cosine
}}
{{eqn | r = a u \frac x a - a \ln \size {\sec u} + C
      | c = Substitution for $\tan u$ from $\paren 1$
}}
{{eqn | r = a u \frac x a - a \ln \size {\sqrt {1 + \frac {x^2} {a^2} } } + C
      | c = Substitution for $\sec u$ from $\paren 2$
}}
{{eqn | r = x \arctan \frac x a - a \ln \size {\sqrt {1 + \frac {x^2} {a^2} } } + C
      | c = Substitution for $u$
}}
{{eqn | r = x \arctan \frac x a - \frac a 2 \ln \size {\frac {x^2 + a^2 } {a^2} } + C
      | c = Logarithm of Power and simplifying
}}
{{eqn | r = x \arctan \frac x a - \frac a 2 \ln \size {x^2 + a^2} - \ln \size {a^2} + C
      | c = Difference of Logarithms
}}
{{eqn | r = x \arctan \frac x a - \frac a 2 \ln \size {x^2 + a^2} + C
      | c = subsuming $\ln \size {a^2}$ into arbitrary constant
}}
{{eqn | r = x \arctan \frac x a - \frac a 2 \map \ln {x^2 + a^2} + C
      | c = $x^2 + a^2$ always positive
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arctangent of x over a

:$\ds \int \arctan \frac x a \rd x = x \arctan \frac x a - \frac a 2 \map \ln {x^2 + a^2} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac a {x^2 + a^2}
      | c = Derivative of $\arctan \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = x
      | c = Primitive of Constant
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arctan \frac x a \rd x
      | r = x \arctan \frac x a - \int x \paren {\frac a {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x \arctan \frac x a - a \int \frac {x \rd x} {x^2 + a^2} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = x \arctan \frac x a - a \paren {\frac 1 2 \ln \paren {x^2 + a^2} } + C
      | c = Primitive of $\dfrac x {x^2 + a^2}$
}}
{{eqn | r = x \arctan \frac x a - \frac a 2 \ln \paren {x^2 + a^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arctangent of x over a

:$\ds \int \arctan \frac x a \rd x = x \arctan \frac x a - \frac a 2 \map \ln {x^2 + a^2} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \arctan x \rd x
      | r = x \arctan x - \frac {\map \ln {x^2 + 1} } 2 + C
      | c = Primitive of $\arctan x$
}}
{{eqn | ll= \leadsto
      | l = \int \arctan \frac x a \rd x
      | r = \frac 1 {1 / a} \paren {\frac x a \arctan \frac x a - \dfrac 1 2 \map \ln {\paren {\frac x a}^2 + 1} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = x \arctan \frac x a - \frac a 2 \map \ln {x^2 + a^2} + C
      | c = after simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Arctangent of x over a

:$\ds \int x \arctan \frac x a \rd x = \frac {x^2 + a^2} 2 \arctan \frac x a - \frac {a x} 2 + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac a {x^2 + a^2}
      | c = Derivative of $\arctan \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^2} 2
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \arctan \frac x a \rd x
      | r = \frac {x^2} 2 \arctan \frac x a - \int \frac {x^2} 2 \paren {\frac a {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^2} 2 \arctan \frac x a - \frac a 2 \int \frac {x^2 \rd x} {x^2 + a^2} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^2} 2 \arctan \frac x a - \frac a 2 \paren {x - a \arctan \frac x a} + C
      | c = Primitive of $\dfrac {x^2} {x^2 + a^2}$
}}
{{eqn | r = \frac {x^2 + a^2} 2 \arctan \frac x a - \frac {a x} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Arccotangent of x over a

:$\ds \int x \arccot \frac x a \rd x = \frac {x^2 + a^2} 2 \arccot \frac x a + \frac {a x} 2 + C$

Proof:
<onlyinclude>
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccot \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x^2 + a^2}
      | c = Derivative of $\arccot \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^2} 2
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \arccot \frac x a \rd x
      | r = \frac {x^2} 2 \arccot \frac x a - \int \frac {x^2} 2 \paren {\frac {-a} {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^2} 2 \arccot \frac x a + \frac a 2 \int \frac {x^2 \rd x} {x^2 + a^2} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^2} 2 \arccot \frac x a + \frac a 2 \paren {x - a \arctan {\frac x a} } + C
      | c = Primitive of $\dfrac {x^2} {x^2 + a^2}$
}}
{{eqn | r = \frac {x^2} 2 \arccot \frac x a + \frac a 2 \paren {x - a \paren {\frac \pi 2 - \arccot {\frac x a} } } + C
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \frac {x^2 + a^2} 2 \arccot \frac x a + \frac {a x} 2 - \frac {a^2 \pi} 2 + C
      | c = simplifying
}}
{{eqn | r = \frac {x^2 + a^2} 2 \arccot \frac x a + \frac {a x} 2 + C
      | c = subsuming $\dfrac {a^2 \pi} 2$ into the arbitrary constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x squared by Arctangent of x over a

:$\ds \int x^2 \arctan \frac x a \rd x = \frac {x^3} 3 \arctan \frac x a - \frac {a x^2} 6 + \frac {a^3} 6 \map \ln {x^2 + a^2} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac a {x^2 + a^2}
      | c = Derivative of $\arctan \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^3} 3
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^2 \arctan \frac x a \rd x
      | r = \frac {x^3} 3 \arctan \frac x a - \int \frac {x^3} 3 \paren {\frac a {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^3} 3 \arctan \frac x a - \frac a 3 \int \frac {x^3 \rd x} {x^2 + a^2} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^3} 3 \arctan \frac x a - \frac a 3 \paren {\frac {x^2} 2 - \frac {a^2} 2 \map \ln {x^2 + a^2} } + C
      | c = Primitive of $\dfrac {x^3} {x^2 + a^2}$
}}
{{eqn | r = \frac {x^3} 3 \arctan \frac x a - \frac {a x^2} 6 + \frac {a^3} 6 \map \ln {x^2 + a^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x squared by Arccotangent of x over a

:$\ds \int x^2 \arccot \frac x a \rd x = \frac {x^3} 3 \arccot \frac x a + \frac {a x^2} 6 - \frac {a^3} 6 \map \ln {x^2 + a^2} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccot \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x^2 + a^2}
      | c = Derivative of $\arccot \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^3} 3
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^2 \arccot \frac x a \rd x
      | r = \frac {x^3} 3 \arccot \frac x a - \int \frac {x^3} 3 \paren {\frac {-a} {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^3} 3 \arccot \frac x a + \frac a 3 \int \frac {x^3 \rd x} {x^2 + a^2} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^3} 3 \arccot \frac x a + \frac a 3 \paren {\frac {x^2} 2 - \frac {a^2} 2 \map \ln {x^2 + a^2} } + C
      | c = Primitive of $\dfrac {x^3} {x^2 + a^2}$
}}
{{eqn | r = \frac {x^3} 3 \arccot \frac x a + \frac {a x^2} 6 - \frac {a^3} 6 \map \ln {x^2 + a^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccotangent of x over a over x

:$\ds \int \dfrac 1 x \arccot \frac x a \rd x = \frac \pi 2 \ln \size x - \int \dfrac 1 x \arctan \frac x a \rd x$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac 1 x \arccot \frac x a \rd x
      | r = \int \dfrac 1 x \paren {\frac \pi 2 - \arctan \frac x a} \rd x
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \frac \pi 2 \int \frac {\d x} x - \int \dfrac 1 x \arctan \frac x a \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac \pi 2 \ln \size x - \int \dfrac 1 x \arctan \frac x a \rd x + C
      | c = Primitive of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arctangent of x over a over x squared

:$\ds \int \frac 1 {x^2} \arctan \frac x a \rd x = -\frac 1 x \arctan \frac x a - \frac 1 {2 a} \map \ln {\frac {x^2 + a^2} {x^2} } + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac a {x^2 + a^2}
      | c = Derivative of $\arctan \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-1} x
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac 1 {x^2} \arctan \frac x a \rd x
      | r = \arctan \frac x a \paren {\frac {-1} x} - \int \paren {\frac {-1} x} \paren {\frac a {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = -\frac 1 x \arctan \frac x a + a \int \frac {\d x} {x \paren {x^2 + a^2} } \rd x + C
      | c = simplifying
}}
{{eqn | r = -\frac 1 x \arctan \frac x a + \frac 1 a \paren {\frac 1 {2 a^2} \map \ln {\frac {x^2} {x^2 + a^2} } } + C
      | c = Primitive of $\dfrac 1 {x \paren {x^2 + a^2} }$
}}
{{eqn | r = -\frac 1 x \arctan \frac x a - \frac 1 {2 a} \map \ln {\frac {x^2 + a^2} {x^2} } + C
      | c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccotangent of x over a over x squared

:$\ds \int \frac 1 {x^2} \arccot \frac x a \rd x = -\frac 1 x \arccot \frac x a + \frac 1 {2 a} \map \ln {\frac {x^2 + a^2} {x^2} } + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccot \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x^2 + a^2}
      | c = Derivative of $\arccot \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-1} x
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac 1 {x^2} \arccot \frac x a
      | r = \arccot \frac x a \paren {\frac {-1} x} - \int \paren {\frac {-1} x} \paren {\frac {-a} {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = -\frac 1 x \arccot \frac x a - a \int \frac {\d x} {x \paren {x^2 + a^2} } \rd x + C
      | c = simplifying
}}
{{eqn | r = -\frac 1 x \arccot \frac x a - \frac 1 a \paren {\frac 1 {2 a^2} \map \ln {\frac {x^2} {x^2 + a^2} } } + C
      | c = Primitive of $\dfrac 1 {x \paren {x^2 + a^2} }$
}}
{{eqn | r = -\frac 1 x \arccot \frac x a + \frac 1 {2 a} \map \ln {\frac {x^2 + a^2} {x^2} } + C
      | c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccotangent of x over a

:$\ds \int \arccot \frac x a \rd x = x \arccot \frac x a + \frac a 2 \map \ln {x^2 + a^2} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccot \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cot u 
      | r = \frac x a
      | c = {{Defof|Arccotangent}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \csc u 
      | r = \sqrt {1 + \frac {x^2} {a^2} }
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arccot \frac x a \rd x
      | r = -a \int u \csc^2 u \rd u
      | c = Primitive of Function of Arccotangent
}}
{{eqn | r = -a \paren {-u \cot u + \ln \size {\sin u} } + C
      | c = Primitive of $x \csc^2 a x$ with $a = 1$
}}
{{eqn | r = a u \cot u - a \ln \size {\sin u} + C
      | c = simplifying
}}
{{eqn | r = a u \cot u + a \ln \size {\csc u} + C
      | c = Logarithm of Reciprocal and Cosecant is Reciprocal of Sine
}}
{{eqn | r = a u \frac x a + a \ln \size {\csc u} + C
      | c = Substitution for $\cot u$ from $(1)$
}}
{{eqn | r = x u + a \ln \size {\sqrt {1 + \frac {x^2} {a^2} } } + C
      | c = Substitution for $\csc u$ from $(2)$
}}
{{eqn | r = x \arccot \frac x a + a \ln \size {\sqrt {1 + \frac {x^2} {a^2} } } + C
      | c = Substitution for $u$
}}
{{eqn | r = x \arccot \frac x a + \frac a 2 \ln \size {\frac {x^2 + a^2 } {a^2} } + C
      | c = Logarithm of Power and simplifying
}}
{{eqn | r = x \arccot \frac x a + \frac a 2 \ln \size {x^2 + a^2} - \ln \size {a^2} + C
      | c = Difference of Logarithms
}}
{{eqn | r = x \arccot \frac x a + \frac a 2 \ln \size {x^2 + a^2} + C
      | c = subsuming $\ln \size {a^2}$ into arbitrary constant
}}
{{eqn | r = x \arccot \frac x a + \frac a 2 \, \map \ln {x^2 + a^2} + C
      | c = $x^2 + a^2$ always positive
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccotangent of x over a

:$\ds \int \arccot \frac x a \rd x = x \arccot \frac x a + \frac a 2 \map \ln {x^2 + a^2} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccot \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x^2 + a^2}
      | c = Derivative of $\arccot  \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = x
      | c = Primitive of Constant
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arccot \frac x a \rd x
      | r = x \arccot \frac x a - \int x \paren {\frac {-a} {x^2 + a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x \arccot \frac x a + a \int \frac {x \rd x} {x^2 + a^2} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = x \arccot \frac x a + a \paren {\frac 1 2 \map \ln {x^2 + a^2} } + C
      | c = Primitive of $\dfrac x {x^2 + a^2}$
}}
{{eqn | r = x \arccot \frac x a + \frac a 2 \map \ln {x^2 + a^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}