I have been trying to use the Method of Coefficients in some combinatorial arguments. Since the result ended up being more complicated than I am comfortable with I would like to know if there is information that would at least allow me to phrase the axioms and set the syntax; and of course ask it whether my reasoning is good. Even better would be an actual implementation!
I have found the Isabelle Formal Power Series and Binomial theory
https://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/HOL-Library/Formal_Power_Series.html
http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/HOL-Algebra/Binomial.html
Progress: I am down to proving Lagrange's inversion theorem. Which is giving me problems.
Which I hope will allow me to state, in an intuitive manner, the "Method of Coefficients" as used in combinatorics/binomial sequences, as Axioms or Theorems. Since I am not familiar with Isabelle, the "Method of Coefficients" might already be in there.