int_rules_4_7_3 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 4.7.3*Secant*normalization*rules =#
    @apply_utils Antiderivative(~u * (~(c') * sin(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * csc(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (~c * sin(~a + ~b * ~x)) ^ ~m * (~d * csc(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) * (~d * csc(~a + ~b * ~x)) ^ (~n - ~m), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(c') * cos(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * sec(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (~c * cos(~a + ~b * ~x)) ^ ~m * (~d * sec(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) * (~d * sec(~a + ~b * ~x)) ^ (~n - ~m), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * sec(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (((~c * tan(~a + ~b * ~x)) ^ ~m * (~d * csc(~a + ~b * ~x)) ^ ~m) / (~d * sec(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~d * sec(~a + ~b * ~x)) ^ (~m + ~n)) / (~d * csc(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && (KnownSecantIntegrandQ(~u, ~x) && Not(IntegerQ(~m)))
    @apply_utils Antiderivative(~u * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * csc(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (((~c * tan(~a + ~b * ~x)) ^ ~m * (~d * csc(~a + ~b * ~x)) ^ ~m) / (~d * sec(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~d * sec(~a + ~b * ~x)) ^ ~m) / (~d * csc(~a + ~b * ~x)) ^ (~m - ~n), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && (KnownSecantIntegrandQ(~u, ~x) && Not(IntegerQ(~m)))
    @apply_utils Antiderivative(~u * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * sec(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (((~c * cot(~a + ~b * ~x)) ^ ~m * (~d * sec(~a + ~b * ~x)) ^ ~m) / (~d * csc(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~d * csc(~a + ~b * ~x)) ^ ~m) / (~d * sec(~a + ~b * ~x)) ^ (~m - ~n), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && (KnownSecantIntegrandQ(~u, ~x) && Not(IntegerQ(~m)))
    @apply_utils Antiderivative(~u * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(m') * (~(d') * csc(~(a') + ~(b') * ~x)) ^ ~(n'), ~x) => (((~c * cot(~a + ~b * ~x)) ^ ~m * (~d * sec(~a + ~b * ~x)) ^ ~m) / (~d * csc(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~d * csc(~a + ~b * ~x)) ^ (~m + ~n)) / (~d * sec(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x) && (KnownSecantIntegrandQ(~u, ~x) && Not(IntegerQ(~m)))
    @apply_utils Antiderivative(~u * (~(c') * sin(~(a') + ~(b') * ~x)) ^ ~(m'), ~x) => (~c * csc(~a + ~b * ~x)) ^ ~m * (~c * sin(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) / (~c * csc(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~m], ~x) && (Not(IntegerQ(~m)) && KnownSecantIntegrandQ(~u, ~x))
    @apply_utils Antiderivative(~u * (~(c') * cos(~(a') + ~(b') * ~x)) ^ ~(m'), ~x) => (~c * cos(~a + ~b * ~x)) ^ ~m * (~c * sec(~a + ~b * ~x)) ^ ~m * Antiderivative(ActivateTrig(~u) / (~c * sec(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~m], ~x) && (Not(IntegerQ(~m)) && KnownSecantIntegrandQ(~u, ~x))
    @apply_utils Antiderivative(~u * (~(c') * tan(~(a') + ~(b') * ~x)) ^ ~(m'), ~x) => (((~c * tan(~a + ~b * ~x)) ^ ~m * (~c * csc(~a + ~b * ~x)) ^ ~m) / (~c * sec(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~c * sec(~a + ~b * ~x)) ^ ~m) / (~c * csc(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~m], ~x) && (Not(IntegerQ(~m)) && KnownSecantIntegrandQ(~u, ~x))
    @apply_utils Antiderivative(~u * (~(c') * cot(~(a') + ~(b') * ~x)) ^ ~(m'), ~x) => (((~c * cot(~a + ~b * ~x)) ^ ~m * (~c * sec(~a + ~b * ~x)) ^ ~m) / (~c * csc(~a + ~b * ~x)) ^ ~m) * Antiderivative((ActivateTrig(~u) * (~c * csc(~a + ~b * ~x)) ^ ~m) / (~c * sec(~a + ~b * ~x)) ^ ~m, ~x) <-- FreeQ([~a, ~b, ~c, ~m], ~x) && (Not(IntegerQ(~m)) && KnownSecantIntegrandQ(~u, ~x))
    @apply_utils Antiderivative(~u * (~(c') * sec(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(B') * cos(~(a') + ~(b') * ~x)), ~x) => ~c * Antiderivative(ActivateTrig(~u) * (~c * sec(~a + ~b * ~x)) ^ (~n - 1) * (~B + ~A * sec(~a + ~b * ~x)), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(c') * csc(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(B') * sin(~(a') + ~(b') * ~x)), ~x) => ~c * Antiderivative(ActivateTrig(~u) * (~c * csc(~a + ~b * ~x)) ^ (~n - 1) * (~B + ~A * csc(~a + ~b * ~x)), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(B') * cos(~(a') + ~(b') * ~x)), ~x) => Antiderivative((ActivateTrig(~u) * (~B + ~A * sec(~a + ~b * ~x))) / sec(~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~A, ~B], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(B') * sin(~(a') + ~(b') * ~x)), ~x) => Antiderivative((ActivateTrig(~u) * (~B + ~A * csc(~a + ~b * ~x))) / csc(~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~A, ~B], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * sec(~(a') + ~(b') * ~x)) ^ ~(n') * (~(A') + ~(B') * cos(~(a') + ~(b') * ~x) + ~(C') * cos(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * sec(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~B * sec(~a + ~b * ~x) + ~A * sec(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~C, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * csc(~(a') + ~(b') * ~x)) ^ ~(n') * (~(A') + ~(B') * sin(~(a') + ~(b') * ~x) + ~(C') * sin(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * csc(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~B * csc(~a + ~b * ~x) + ~A * csc(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~B, ~C, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * sec(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(C') * cos(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * sec(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~A * sec(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~C, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~(u') * (~(c') * csc(~(a') + ~(b') * ~x)) ^ ~(n') * (~A + ~(C') * sin(~(a') + ~(b') * ~x) ^ 2), ~x) => (~c) ^ 2 * Antiderivative(ActivateTrig(~u) * (~c * csc(~a + ~b * ~x)) ^ (~n - 2) * (~C + ~A * csc(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~A, ~C, ~n], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(A') + ~(B') * cos(~(a') + ~(b') * ~x) + ~(C') * cos(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~B * sec(~a + ~b * ~x) + ~A * sec(~a + ~b * ~x) ^ 2)) / sec(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(A') + ~(B') * sin(~(a') + ~(b') * ~x) + ~(C') * sin(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~B * csc(~a + ~b * ~x) + ~A * csc(~a + ~b * ~x) ^ 2)) / csc(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(C') * cos(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~A * sec(~a + ~b * ~x) ^ 2)) / sec(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~C], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~A + ~(C') * sin(~(a') + ~(b') * ~x) ^ 2), ~x) => Antiderivative((ActivateTrig(~u) * (~C + ~A * csc(~a + ~b * ~x) ^ 2)) / csc(~a + ~b * ~x) ^ 2, ~x) <-- FreeQ([~a, ~b, ~A, ~C], ~x) && KnownSecantIntegrandQ(~u, ~x)
    @apply_utils Antiderivative(~u * (~(A') * sec(~(a') + ~(b') * ~x) ^ ~(n') + ~(B') * sec(~(a') + ~(b') * ~x) ^ ~n1 + ~(C') * sec(~(a') + ~(b') * ~x) ^ ~n2), ~x) => Antiderivative(ActivateTrig(~u) * sec(~a + ~b * ~x) ^ ~n * (~A + ~B * sec(~a + ~b * ~x) + ~C * sec(~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') * csc(~(a') + ~(b') * ~x) ^ ~(n') + ~(B') * csc(~(a') + ~(b') * ~x) ^ ~n1 + ~(C') * csc(~(a') + ~(b') * ~x) ^ ~n2), ~x) => Antiderivative(ActivateTrig(~u) * csc(~a + ~b * ~x) ^ ~n * (~A + ~B * csc(~a + ~b * ~x) + ~C * csc(~a + ~b * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~A, ~B, ~C, ~n], ~x) && (EqQ(~n1, ~n + 1) && EqQ(~n2, ~n + 2))
end
