How can I code an assumption in axiom?
In my case, I'm analyzing a polynomial differential equation. I want to compute the order of a polynomial at a factor, which is the power of the factor that appears in the polynomial.
For example, consider D(f,x), where f is some unspecified polynomial. I want to write a function "ord" and compute ord(D(f,x), ifac), where ifac is some unspecified irreducible factor. I can't do this calculation with the information given. However, if I assert that ord(f, ifac) > 0, then ord(D(f,x), ifac) = ord(f, ifac) - 1.
In other words, differentiation causes the order of an irreducible factor to drop by one, but only if the factor was actually present in the original polynomial.