Goal:
  
  G : t
  HI : invariants G
  HG : acyclic_no_loop G
  n : Z
  x : V.t
  y : V.t
  Vy : ~ VSet.In y (V G)
  Hle : leq_vertices G n x y
  XX := Hle
          (fun z : V.t =>
           if is_left (V.eq_dec z y)
           then to_label (lsp G (s G) x)
           else to_label (lsp G (s G) z))
          (conj
             (let s0 := V.eq_dec (s G) y in
              match
                s0 as s1
                return
                  ((if is_left s1
                    then to_label (lsp G (s G) x)
                    else to_label (lsp G (s G) (s G))) = 0%nat)
              with
              | left e =>
                  (fun e0 : s G = y =>
                   False_rect
                     ((if is_left (left e0)
                       then to_label (lsp G (s G) x)
                       else to_label (lsp G (s G) (s G))) = 0%nat)
                     (Vy
                        (eq_ind (s G)
                           (fun y : V.t =>
                            ~ VSet.In y (V G) ->
                            leq_vertices G n x y -> VSet.In y (V G))
                           (fun (_ : ~ VSet.In (s G) (V G))
                              (_ : leq_vertices G n x (s G)) =>
                            unkeyed (source_vertex G)) y e0 Vy Hle))) e
              | right n =>
                  (fun _ : s G <> y =>
                   let H :
                     forall G : t,
                     invariants G ->
                     acyclic_no_loop G ->
                     to_label (lsp G (s G) (s G)) = 0%nat :=
                     fun (G : t) (HI : invariants G) (HG : acyclic_no_loop G)
                     => match lsp_correctness G with
                        | conj x _ => x
                        end in
                   H G HI HG) n
              end)
             (fun (e : EdgeSet.elt) (H : EdgeSet.In e (E G)) =>
              let s0 := V.eq_dec e..s y in
              match
                s0 as s1
                return
                  (Z.of_nat
                     (if is_left s1
                      then to_label (lsp G (s G) x)
                      else to_label (lsp G (s G) e..s)) + e..w <=
                   Z.of_nat
                     (if is_left (V.eq_dec e..t y)
                      then to_label (lsp G (s G) x)
                      else to_label (lsp G (s G) e..t)))
              with
              | left e0 =>
                  (fun e1 : e..s = y =>
                   False_rect
                     (Z.of_nat
                        (if is_left (left e1)
                         then to_label (lsp G (s G) x)
                         else to_label (lsp G (s G) e..s)) + e..w <=
                      Z.of_nat
                        (if is_left (V.eq_dec e..t y)
                         then to_label (lsp G (s G) x)
                         else to_label (lsp G (s G) e..t)))
                     (Vy
                        (eq_ind e..s
                           (fun y : V.t =>
                            ~ VSet.In y (V G) ->
                            leq_vertices G n x y -> VSet.In y (V G))
                           (fun (_ : ~ VSet.In e..s (V G))
                              (_ : leq_vertices G n x e..s) =>
                            let H0 :
                              forall e2 : EdgeSet.elt,
                              EdgeSet.In e2 (E G) ->
                              VSet.In e2..s (V G) /\ VSet.In e2..t (V G) :=
                              edges_vertices G in
                            let H1 :
                              forall e2 : EdgeSet.elt,
                              EdgeSet.In e2 (E G) -> VSet.In e2..s (V G) :=
                              fun (e2 : EdgeSet.elt)
                                (H1 : EdgeSet.In e2 (E G)) =>
                              match H0 e2 H1 with
                              | conj x _ => x
                              end in
                            H1 e H) y e1 Vy Hle))) e0
              | right n0 =>
                  (fun n1 : e..s <> y =>
                   let s1 := V.eq_dec e..t y in
                   match
                     s1 as s2
                     return
                       (Z.of_nat
                          (if is_left (right n1)
                           then to_label (lsp G (s G) x)
                           else to_label (lsp G (s G) e..s)) + e..w <=
                        Z.of_nat
                          (if is_left s2
                           then to_label (lsp G (s G) x)
                           else to_label (lsp G (s G) e..t)))
                   with
                   | left e0 =>
                       (fun e1 : e..t = y =>
                        False_rect
                          (Z.of_nat
                             (if is_left (right n1)
                              then to_label (lsp G (s G) x)
                              else to_label (lsp G (s G) e..s)) + e..w <=
                           Z.of_nat
                             (if is_left (left e1)
                              then to_label (lsp G (s G) x)
                              else to_label (lsp G (s G) e..t)))
                          (Vy
                             (eq_ind e..t
                                (fun y : V.t =>
                                 ~ VSet.In y (V G) ->
                                 leq_vertices G n x y ->
                                 e..s <> y -> VSet.In y (V G))
                                (fun (_ : ~ VSet.In e..t (V G))
                                   (_ : leq_vertices G n x e..t)
                                   (_ : e..s <> e..t) =>
                                 let H0 :
                                   forall e2 : EdgeSet.elt,
                                   EdgeSet.In e2 (E G) ->
                                   VSet.In e2..s (V G) /\ VSet.In e2..t (V G) :=
                                   edges_vertices G in
                                 let H1 :
                                   forall e2 : EdgeSet.elt,
                                   EdgeSet.In e2 (E G) -> VSet.In e2..t (V G) :=
                                   fun (e2 : EdgeSet.elt)
                                     (H1 : EdgeSet.In e2 (E G)) =>
                                   match H0 e2 H1 with
                                   | conj _ x0 => x0
                                   end in
                                 H1 e H) y e1 Vy Hle n1))) e0
                   | right n =>
                       (fun _ : e..t <> y =>
                        let H0 :
                          forall G : t,
                          invariants G ->
                          acyclic_no_loop G ->
                          forall e0 : EdgeSet.elt,
                          EdgeSet.In e0 (E G) ->
                          Z.of_nat (to_label (lsp G (s G) e0..s)) + e0..w <=
                          Z.of_nat (to_label (lsp G (s G) e0..t)) :=
                          fun (G : t) (HI : invariants G)
                            (HG : acyclic_no_loop G) =>
                          match lsp_correctness G with
                          | conj _ x0 => x0
                          end in
                        H0 G HI HG e H) n
                   end) n0
              end))
     : Z.of_nat
         ((fun z : V.t =>
           if is_left (V.eq_dec z y)
           then to_label (lsp G (s G) x)
           else to_label (lsp G (s G) z)) x) + n <=
       Z.of_nat
         ((fun z : V.t =>
           if is_left (V.eq_dec z y)
           then to_label (lsp G (s G) x)
           else to_label (lsp G (s G) z)) y)
  ============================
   (n <= 0)


DEBUG:Going to execute:
clearbody XX