int_rules_1_3_1 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 1.3.1*P(x)^p =#
    @apply_utils Antiderivative(~(u') * (~P) ^ ~p * (~Q) ^ ~q, ~x) => Module([gcd = PolyGCD(~P, ~Q, ~x)], Antiderivative(~u * gcd ^ (~p + ~q) * PolynomialQuotient(~P, gcd, ~x) ^ ~p * PolynomialQuotient(~Q, gcd, ~x) ^ ~q, ~x) <-- NeQ(gcd, 1)) <-- IGtQ(~p, 0) && (ILtQ(~q, 0) && (PolyQ(~P, ~x) && PolyQ(~Q, ~x)))
    @apply_utils Antiderivative(~(u') * ~P * (~Q) ^ ~q, ~x) => Module([gcd = PolyGCD(~P, ~Q, ~x)], Antiderivative(~u * gcd ^ (~q + 1) * PolynomialQuotient(~P, gcd, ~x) * PolynomialQuotient(~Q, gcd, ~x) ^ ~q, ~x) <-- NeQ(gcd, 1)) <-- ILtQ(~q, 0) && (PolyQ(~P, ~x) && PolyQ(~Q, ~x))
    @apply_utils Antiderivative(~(u') * (~P) ^ ~(p'), ~x) => With([m = MinimumMonomialExponent(~P, ~x)], ((~P) ^ FracPart(~p) / ((~x) ^ (m * FracPart(~p)) * Distrib(1 / (~x) ^ m, ~P) ^ FracPart(~p))) * Antiderivative(~u * (~x) ^ (m * ~p) * Distrib(1 / (~x) ^ m, ~P) ^ ~p, ~x)) <-- FreeQ(~p, ~x) && (Not(IntegerQ(~p)) && (SumQ(~P) && (EveryQ(Function(BinomialQ(Symbol("#1"), ~x)), ~P) && Not(PolyQ(~P, ~x, 2)))))
    @apply_utils Antiderivative((~P) ^ ~p, ~x) => With([u = Factor(ReplaceAll(~P, (~x->begin
                                        #= none:1 =#
                                        #= none:3 =#
                                        sqrt(~x)
                                    end)))], Antiderivative(ExpandIntegrand(ReplaceAll(u, (~x->begin
                                            #= none:4 =#
                                            #= none:6 =#
                                            (~x) ^ 2
                                        end)) ^ ~p, ~x), ~x) <-- Not(SumQ(NonfreeFactors(u, ~x)))) <-- PolyQ(~P, (~x) ^ 2) && ILtQ(~p, 0)
    @apply_utils Antiderivative((~P) ^ ~p, ~x) => With([u = Factor(~P)], Antiderivative(ExpandIntegrand(u ^ ~p, ~x), ~x) <-- Not(SumQ(NonfreeFactors(u, ~x)))) <-- PolyQ(~P, ~x) && ILtQ(~p, 0)
    @apply_utils Antiderivative((~P) ^ ~p, ~x) => With([u = Factor(~P)], Antiderivative(u ^ ~p, ~x) <-- Not(SumQ(NonfreeFactors(u, ~x)))) <-- PolyQ(~P, ~x) && IntegerQ(~p)
    #= Antiderivative((~Pn)^(~p),~x) := With([u=Factor(Pn)], Pn^p/DistributeDegree(u,p)*Antiderivative(DistributeDegree(u,p),x) <--  Not(SumQ(u))) <-- PolyQ(Pn,x) && Not(IntegerQ(p)) =#
    @apply_utils Antiderivative((~(a') + ~(b') * ~x + ~(c') * (~x) ^ 2 + ~(d') * (~x) ^ 3) ^ ~p, ~x) => (1 / 3 ^ ~p) * Subst(Antiderivative(Simp((3 * ~a * ~c - (~b) ^ 2) / ~c + ((~c) ^ 2 * (~x) ^ 3) / ~b, ~x) ^ ~p, ~x), ~x, ~c / (3 * ~d) + ~x) <-- FreeQ([~a, ~b, ~c, ~d], ~x) && (IGtQ(~p, 0) && EqQ((~c) ^ 2 - 3 * ~b * ~d, 0))
    @apply_utils Antiderivative((~P) ^ ~p, ~x) => Antiderivative(ExpandToSum((~P) ^ ~p, ~x), ~x) <-- PolyQ(~P, ~x) && IGtQ(~p, 0)
    @apply_utils Antiderivative((~P) ^ ~p, ~x) => Antiderivative(ExpandIntegrand((~P) ^ ~p, ~x), ~x) <-- PolyQ(~P, ~x) && (IntegerQ(~p) && QuadraticProductQ(Factor(~P), ~x))
    @apply_utils Antiderivative((~(a') + ~(b') * ~x + ~(d') * (~x) ^ 3) ^ ~p, ~x) => (1 / (3 ^ (3 * ~p) * (~a) ^ (2 * ~p))) * Antiderivative((3 * ~a - ~b * ~x) ^ ~p * (3 * ~a + 2 * ~b * ~x) ^ (2 * ~p), ~x) <-- FreeQ([~a, ~b, ~d], ~x) && (EqQ(4 * (~b) ^ 3 + 27 * (~a) ^ 2 * ~d, 0) && IntegerQ(~p))
    @apply_utils Antiderivative((~(a') + ~(b') * ~x + ~(d') * (~x) ^ 3) ^ ~p, ~x) => ((~a + ~b * ~x + ~d * (~x) ^ 3) ^ ~p / ((3 * ~a - ~b * ~x) ^ ~p * (3 * ~a + 2 * ~b * ~x) ^ (2 * ~p))) * Antiderivative((3 * ~a - ~b * ~x) ^ ~p * (3 * ~a + 2 * ~b * ~x) ^ (2 * ~p), ~x) <-- FreeQ([~a, ~b, ~d, ~p], ~x) && (EqQ(4 * (~b) ^ 3 + 27 * (~a) ^ 2 * ~d, 0) && Not(IntegerQ(~p)))
    @apply_utils Antiderivative((~(a') + ~(b') * ~x + ~(d') * (~x) ^ 3) ^ ~p, ~x) => With([r = Rt(-9 * ~a * (~d) ^ 2 + sqrt(3) * ~d * sqrt(4 * (~b) ^ 3 * ~d + 27 * (~a) ^ 2 * (~d) ^ 2), 3)], (1 / (~d) ^ (2 * ~p)) * Antiderivative(Simp(((18 ^ (1 / 3) * ~b * ~d) / (3r) - r / 18 ^ (1 / 3)) + ~d * ~x, ~x) ^ ~p * Simp((((~b * ~d) / 3 + (12 ^ (1 / 3) * (~b) ^ 2 * (~d) ^ 2) / (3 * r ^ 2) + r ^ 2 / (3 * 12 ^ (1 / 3))) - ~d * ((2 ^ (1 / 3) * ~b * ~d) / (3 ^ (1 / 3) * r) - r / 18 ^ (1 / 3)) * ~x) + (~d) ^ 2 * (~x) ^ 2, ~x) ^ ~p, ~x)) <-- FreeQ([~a, ~b, ~d], ~x) && (NeQ(4 * (~b) ^ 3 + 27 * (~a) ^ 2 * ~d, 0) && IntegerQ(~p))
    @apply_utils Antiderivative((~(a') + ~(b') * ~x + ~(d') * (~x) ^ 3) ^ ~p, ~x) => With([r = Rt(-9 * ~a * (~d) ^ 2 + sqrt(3) * ~d * sqrt(4 * (~b) ^ 3 * ~d + 27 * (~a) ^ 2 * (~d) ^ 2), 3)], ((~a + ~b * ~x + ~d * (~x) ^ 3) ^ ~p / (Simp(((18 ^ (1 / 3) * ~b * ~d) / (3r) - r / 18 ^ (1 / 3)) + ~d * ~x, ~x) ^ ~p * Simp((((~b * ~d) / 3 + (12 ^ (1 / 3) * (~b) ^ 2 * (~d) ^ 2) / (3 * r ^ 2) + r ^ 2 / (3 * 12 ^ (1 / 3))) - ~d * ((2 ^ (1 / 3) * ~b * ~d) / (3 ^ (1 / 3) * r) - r / 18 ^ (1 / 3)) * ~x) + (~d) ^ 2 * (~x) ^ 2, ~x) ^ ~p)) * Antiderivative(Simp(((18 ^ (1 / 3) * ~b * ~d) / (3r) - r / 18 ^ (1 / 3)) + ~d * ~x, ~x) ^ ~p * Simp((((~b * ~d) / 3 + (12 ^ (1 / 3) * (~b) ^ 2 * (~d) ^ 2) / (3 * r ^ 2) + r ^ 2 / (3 * 12 ^ (1 / 3))) - ~d * ((2 ^ (1 / 3) * ~b * ~d) / (3 ^ (1 / 3) * r) - r / 18 ^ (1 / 3)) * ~x) + (~d) ^ 2 * (~x) ^ 2, ~x) ^ ~p, ~x)) <-- FreeQ([~a, ~b, ~d, ~p], ~x) && (NeQ(4 * (~b) ^ 3 + 27 * (~a) ^ 2 * ~d, 0) && Not(IntegerQ(~p)))
    @apply_utils Antiderivative((~P3) ^ ~p, ~x) => With([a = Coeff(~P3, ~x, 0), b = Coeff(~P3, ~x, 1), c = Coeff(~P3, ~x, 2), d = Coeff(~P3, ~x, 3)], Subst(Antiderivative(Simp((((2 * c ^ 3 - 9 * b * c * d) + 27 * a * d ^ 2) / (27 * d ^ 2) - ((c ^ 2 - 3 * b * d) * ~x) / (3d)) + d * (~x) ^ 3, ~x) ^ ~p, ~x), ~x, ~x + c / (3d)) <-- NeQ(c, 0)) <-- FreeQ(~p, ~x) && PolyQ(~P3, ~x, 3)
    @apply_utils Antiderivative((~P4) ^ ~p, ~x) => With([a = Coeff(~P4, ~x, 0), b = Coeff(~P4, ~x, 1), c = Coeff(~P4, ~x, 2), d = Coeff(~P4, ~x, 3), e = Coeff(~P4, ~x, 4)], (1 / a ^ (3 * ~p)) * Antiderivative(ExpandIntegrand((a - b * ~x) ^ -(~p) / (a ^ 5 - b ^ 5 * (~x) ^ 5) ^ -(~p), ~x), ~x) <-- NeQ(a, 0) && (EqQ(c, b ^ 2 / a) && (EqQ(d, b ^ 3 / a ^ 2) && EqQ(e, b ^ 4 / a ^ 3)))) <-- FreeQ(~p, ~x) && (PolyQ(~P4, ~x, 4) && ILtQ(~p, 0))
    @apply_utils Antiderivative((~P4) ^ ~p, ~x) => With([a = Coeff(~P4, ~x, 0), b = Coeff(~P4, ~x, 1), c = Coeff(~P4, ~x, 2), d = Coeff(~P4, ~x, 3), e = Coeff(~P4, ~x, 4)], -16 * a ^ 2 * Subst(Antiderivative((1 / (b - 4 * a * ~x) ^ 2) * ((a * (((((-3 * b ^ 4 + 16 * a * b ^ 2 * c) - 64 * a ^ 2 * b * d) + 256 * a ^ 3 * e) - 32 * a ^ 2 * (3 * b ^ 2 - 8 * a * c) * (~x) ^ 2) + 256 * a ^ 4 * (~x) ^ 4)) / (b - 4 * a * ~x) ^ 4) ^ ~p, ~x), ~x, b / (4a) + 1 / ~x) <-- NeQ(a, 0) && (NeQ(b, 0) && EqQ((b ^ 3 - 4 * a * b * c) + 8 * a ^ 2 * d, 0))) <-- FreeQ(~p, ~x) && (PolyQ(~P4, ~x, 4) && (IntegerQ(2 * ~p) && Not(IGtQ(~p, 0))))
    @apply_utils Antiderivative((~Q6) ^ ~p, ~x) => With([a = Coeff(~Q6, ~x, 0), b = Coeff(~Q6, ~x, 2), c = Coeff(~Q6, ~x, 3), d = Coeff(~Q6, ~x, 4), e = Coeff(~Q6, ~x, 6)], (1 / (3 ^ (3 * ~p) * a ^ (2 * ~p))) * Antiderivative(ExpandIntegrand((3a + 3 * Rt(a, 3) ^ 2 * Rt(c, 3) * ~x + b * (~x) ^ 2) ^ ~p * ((3a - 3 * (-1) ^ (1 / 3) * Rt(a, 3) ^ 2 * Rt(c, 3) * ~x) + b * (~x) ^ 2) ^ ~p * (3a + 3 * (-1) ^ (2 / 3) * Rt(a, 3) ^ 2 * Rt(c, 3) * ~x + b * (~x) ^ 2) ^ ~p, ~x), ~x) <-- EqQ(b ^ 2 - 3 * a * d, 0) && EqQ(b ^ 3 - 27 * a ^ 2 * e, 0)) <-- ILtQ(~p, 0) && (PolyQ(~Q6, ~x, 6) && (EqQ(Coeff(~Q6, ~x, 1), 0) && (EqQ(Coeff(~Q6, ~x, 5), 0) && RationalFunctionQ(u, ~x))))
end
