Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem, ported from HOL Light There is much more that could be added here, assuming I don’t run out of energy! Larry