Main winding number theorem for the fundamental domain boundary

The generalized winding number of fdBoundary around interior points equals -1 (clockwise).

theorem RectHomotopyProof.generalizedWindingNumber_fdBoundary_eq_neg_one (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < HHeight) : generalizedWindingNumber' fdBoundary 0 5 p = -1

For interior points p in the fundamental domain, the generalized winding number of the FD boundary around p equals -1 (clockwise orientation).