Goal:
  
  G : t
  HI : invariants G
  HG : acyclic_no_loop G
  n : Z
  x : V.t
  y : VSet.elt
  Vy : VSet.In y (V G)
  Hle : leq_vertices G n x y
  Vx : ~ VSet.In x (V G)
  XX := Hle
          (fun z : V.t =>
           if is_left (V.eq_dec z x)
           then
            if n <=? 0
            then (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
            else to_label (lsp G (s G) y)
           else to_label (lsp G (s G) z))
          (conj
             (let s0 := V.eq_dec (s G) x in
              match
                s0 as s1
                return
                  ((if is_left s1
                    then
                     if n <=? 0
                     then
                      (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
                     else to_label (lsp G (s G) y)
                    else to_label (lsp G (s G) (s G))) = 0%nat)
              with
              | left e =>
                  (fun e0 : s G = x =>
                   False_rect
                     ((if is_left (left e0)
                       then
                        if n <=? 0
                        then
                         (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) +
                          1)%nat
                        else to_label (lsp G (s G) y)
                       else to_label (lsp G (s G) (s G))) = 0%nat)
                     (Vx
                        (eq_ind (s G)
                           (fun x : V.t =>
                            leq_vertices G n x y ->
                            ~ VSet.In x (V G) -> VSet.In x (V G))
                           (fun (_ : leq_vertices G n (s G) y)
                              (_ : ~ VSet.In (s G) (V G)) =>
                            unkeyed (source_vertex G)) x e0 Hle Vx))) e
              | right n =>
                  (fun _ : s G <> x =>
                   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 x in
              match
                s0 as s1
                return
                  (Z.of_nat
                     (if is_left s1
                      then
                       if n <=? 0
                       then
                        (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) +
                         1)%nat
                       else to_label (lsp G (s G) y)
                      else to_label (lsp G (s G) e..s)) + e..w <=
                   Z.of_nat
                     (if is_left (V.eq_dec e..t x)
                      then
                       if n <=? 0
                       then
                        (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) +
                         1)%nat
                       else to_label (lsp G (s G) y)
                      else to_label (lsp G (s G) e..t)))
              with
              | left e0 =>
                  (fun e1 : e..s = x =>
                   False_rect
                     (Z.of_nat
                        (if is_left (left e1)
                         then
                          if n <=? 0
                          then
                           (Z.to_nat
                              (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
                          else to_label (lsp G (s G) y)
                         else to_label (lsp G (s G) e..s)) + e..w <=
                      Z.of_nat
                        (if is_left (V.eq_dec e..t x)
                         then
                          if n <=? 0
                          then
                           (Z.to_nat
                              (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
                          else to_label (lsp G (s G) y)
                         else to_label (lsp G (s G) e..t)))
                     (Vx
                        (eq_ind e..s
                           (fun x : V.t =>
                            leq_vertices G n x y ->
                            ~ VSet.In x (V G) -> VSet.In x (V G))
                           (fun (_ : leq_vertices G n e..s y)
                              (_ : ~ VSet.In e..s (V G)) =>
                            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) x e1 Hle Vx))) e0
              | right n0 =>
                  (fun n1 : e..s <> x =>
                   let s1 := V.eq_dec e..t x in
                   match
                     s1 as s2
                     return
                       (Z.of_nat
                          (if is_left (right n1)
                           then
                            if n <=? 0
                            then
                             (Z.to_nat
                                (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
                            else to_label (lsp G (s G) y)
                           else to_label (lsp G (s G) e..s)) + e..w <=
                        Z.of_nat
                          (if is_left s2
                           then
                            if n <=? 0
                            then
                             (Z.to_nat
                                (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
                            else to_label (lsp G (s G) y)
                           else to_label (lsp G (s G) e..t)))
                   with
                   | left e0 =>
                       (fun e1 : e..t = x =>
                        False_rect
                          (Z.of_nat
                             (if is_left (right n1)
                              then
                               if n <=? 0
                               then
                                (Z.to_nat
                                   (Z.of_nat (to_label (lsp G (s G) y)) - n) +
                                 1)%nat
                               else to_label (lsp G (s G) y)
                              else to_label (lsp G (s G) e..s)) + e..w <=
                           Z.of_nat
                             (if is_left (left e1)
                              then
                               if n <=? 0
                               then
                                (Z.to_nat
                                   (Z.of_nat (to_label (lsp G (s G) y)) - n) +
                                 1)%nat
                               else to_label (lsp G (s G) y)
                              else to_label (lsp G (s G) e..t)))
                          (Vx
                             (eq_ind e..t
                                (fun x : V.t =>
                                 leq_vertices G n x y ->
                                 ~ VSet.In x (V G) ->
                                 e..s <> x -> VSet.In x (V G))
                                (fun (_ : leq_vertices G n e..t y)
                                   (_ : ~ VSet.In e..t (V G))
                                   (_ : 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) x e1 Hle Vx n1))) e0
                   | right n =>
                       (fun _ : e..t <> x =>
                        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 x)
           then
            if n <=? 0
            then (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
            else to_label (lsp G (s G) y)
           else to_label (lsp G (s G) z)) x) + n <=
       Z.of_nat
         ((fun z : V.t =>
           if is_left (V.eq_dec z x)
           then
            if n <=? 0
            then (Z.to_nat (Z.of_nat (to_label (lsp G (s G) y)) - n) + 1)%nat
            else to_label (lsp G (s G) y)
           else to_label (lsp G (s G) z)) y)
  ============================
   False


DEBUG:Going to execute:
clearbody XX