Goal:
  
  G : t
  x : V.t
  y : V.t
  z : V.t
  e : EdgeOf x y
  q : PathOf y z
  IHq : forall (s : VSet.t) (p : SPath s z y) (s' : VSet.t)
          (Hs : VSet.Equal (VSet.union s (nodes q)) s'),
        0 < weight q + sweight p -> 0 < sweight (simplify q p Hs).π2
  s : VSet.t
  p : SPath s z x
  s' : VSet.t
  Hs : VSet.Equal (VSet.union s (nodes (pathOf_step e q))) s'
  H : 0 < e.π1 + weight q + sweight p
  F0 : false = false -> ~ VSet.In x s
  F1 : false = true -> VSet.In x s
  F2 : false = true ->
       forall s1 s2 : VSet.t,
       VSet.Equal (VSet.union s (VSet.add x s1)) s2 ->
       VSet.Equal (VSet.union s s1) s2
  ============================
   (0 < weight q + (sweight p + e.π1))


DEBUG:Going to execute:
lazymatch Zify.zify_convert_to_euclidean_division_equations_flag
           with
           | true =>
               Zify.zify_internal_to_euclidean_division_equations
           | false => idtac
           end