int_rules_4_7_2 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 4.7.2*Tangent*normalization*rules =#
    @apply_utils Antiderivative(~u * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * tan(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (~c * cot(~a + ~b * ~x)) ^ ~m * (~d * tan(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) * (~d * tan(~a + ~b * ~x)) ^ (~n - ~m), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * cos(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (((~c * tan(~a + ~b * ~x)) ^ ~m * (~d * cos(~a + ~b * ~x)) ^ ~m) / (~d * sin(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~d * sin(~a + ~b * ~x)) ^ ~m) / (~d * cos(~a + ~b * ~x)) ^ (~m - ~n), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(m'), ~x) => (~c * cot(~a + ~b * ~x)) ^ ~m * (~c * tan(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) / (~c * tan(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~m], ~x) && (Not(IntegerQ(~m)) && KnownTangentIntegrandQ(~u, ~x))
    @apply_utils Antiderivative(~u * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(m'), ~x) => (~c * cot(~a + ~b * ~x)) ^ ~m * (~c * tan(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) / (~c * cot(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~m], ~x) && (Not(IntegerQ(~m)) && KnownCotangentIntegrandQ(~u, ~x))
    @apply_utils Antiderivative(~u * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(B') * cot(~(a') + ~(b') * ~x)), ~x) => ~c * Antiderivative(ActivateTrig(~u) * (~c * tan(~a + ~b * ~x)) ^ (~n - 1) * (~B + ~A * tan(~a + ~b * ~x)), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~n], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(B') * tan(~(a') + ~(b') * ~x)), ~x) => ~c * Antiderivative(ActivateTrig(~u) * (~c * cot(~a + ~b * ~x)) ^ (~n - 1) * (~B + ~A * cot(~a + ~b * ~x)), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~n], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(B') * cot(~(a') + ~(b') * ~x)), ~x) => Antiderivative((ActivateTrig(~u) * (~B + ~A * tan(~a + ~b * ~x))) / tan(~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~A, ~B], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(B') * tan(~(a') + ~(b') * ~x)), ~x) => Antiderivative((ActivateTrig(~u) * (~B + ~A * cot(~a + ~b * ~x))) / cot(~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~A, ~B], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(n') * (~(A') + ~(B') * cot(~(a') + ~(b') * ~x) + ~(C') * cot(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * tan(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~B * tan(~a + ~b * ~x) + ~A * tan(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~C, ~n], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(n') * (~(A') + ~(B') * tan(~(a') + ~(b') * ~x) + ~(C') * tan(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * cot(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~B * cot(~a + ~b * ~x) + ~A * cot(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~C, ~n], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(C') * cot(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * tan(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~A * tan(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~C, ~n], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(C') * tan(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * cot(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~A * cot(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~C, ~n], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(A') + ~(B') * cot(~(a') + ~(b') * ~x) + ~(C') * cot(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~B * tan(~a + ~b * ~x) + ~A * tan(~a + ~b * ~x) ^ 2)) / tan(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(A') + ~(B') * tan(~(a') + ~(b') * ~x) + ~(C') * tan(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~B * cot(~a + ~b * ~x) + ~A * cot(~a + ~b * ~x) ^ 2)) / cot(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(C') * cot(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~A * tan(~a + ~b * ~x) ^ 2)) / tan(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~C], ~x) && KnownTangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(C') * tan(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~A * cot(~a + ~b * ~x) ^ 2)) / cot(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~C], ~x) && KnownCotangentIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(A') + ~(B') * tan(~(a') + ~(b') * ~x) + ~(C') * cot(~(a') + ~(b') * ~x)), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~A * tan(~a + ~b * ~x) + ~B * tan(~a + ~b * ~x) ^ 2)) / tan(~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C], ~x)
    @apply_utils Antiderivative(~u * (~(A') * tan(~(a') + ~(b') * ~x) ^ ~(n') + ~(B') * tan(~(a') + ~(b') * ~x) ^ ~n1 + ~(C') * tan(~(a') + ~(b') * ~x) ^ ~n2), ~x) => Antiderivative(ActivateTrig(~u) * tan(~a + ~b * ~x) ^ ~n * (~A + ~B * tan(~a + ~b * ~x) + ~C * tan(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C, ~n], ~x) && (EqQ(~n1, ~n + 1) && EqQ(~n2, ~n + 2))
    @apply_utils Antiderivative(~u * (~(A') * cot(~(a') + ~(b') * ~x) ^ ~(n') + ~(B') * cot(~(a') + ~(b') * ~x) ^ ~n1 + ~(C') * cot(~(a') + ~(b') * ~x) ^ ~n2), ~x) => Antiderivative(ActivateTrig(~u) * cot(~a + ~b * ~x) ^ ~n * (~A + ~B * cot(~a + ~b * ~x) + ~C * cot(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C, ~n], ~x) && (EqQ(~n1, ~n + 1) && EqQ(~n2, ~n + 2))
end
