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
  nneg : n <= 0
  n0 : x <> y
  Hxs : lsp G x (s G) = None
  Vx : ~ VSet.In x (V G)
  XX := Hle
          (fun z : V.t =>
           if is_left (V.eq_dec z y)
           then 0%nat
           else
            if is_left (V.eq_dec z x)
            then (Z.to_nat (- n) + 1)%nat
            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 0%nat
                    else
                     if is_left (V.eq_dec (s G) x)
                     then (Z.to_nat (- n) + 1)%nat
                     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 0%nat
                       else
                        if is_left (V.eq_dec (s G) x)
                        then (Z.to_nat (- n) + 1)%nat
                        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 -> x <> y -> VSet.In y (V G))
                           (fun (_ : ~ VSet.In (s G) (V G))
                              (_ : leq_vertices G n x (s G)) 
                              (_ : x <> s G) => unkeyed (source_vertex G)) y
                           e0 Vy Hle n0))) e
              | right n1 =>
                  (fun n2 : s G <> y =>
                   let s1 := V.eq_dec (s G) x in
                   match
                     s1 as s2
                     return
                       ((if is_left (right n2)
                         then 0%nat
                         else
                          if is_left s2
                          then (Z.to_nat (- n) + 1)%nat
                          else to_label (lsp G (s G) (s G))) = 0%nat)
                   with
                   | left e =>
                       (fun e0 : s G = x =>
                        False_rect
                          ((if is_left (right n2)
                            then 0%nat
                            else
                             if is_left (left e0)
                             then (Z.to_nat (- n) + 1)%nat
                             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 ->
                                 x <> y ->
                                 lsp G x (s G) = None ->
                                 ~ VSet.In x (V G) -> VSet.In x (V G))
                                (fun (_ : leq_vertices G n (s G) y)
                                   (_ : s G <> y)
                                   (_ : lsp G (s G) (s G) = None)
                                   (_ : ~ VSet.In (s G) (V G)) =>
                                 unkeyed (source_vertex G)) x e0 Hle n0 Hxs
                                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) n1
              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 0%nat
                      else
                       if is_left (V.eq_dec e..s x)
                       then (Z.to_nat (- n) + 1)%nat
                       else to_label (lsp G (s G) e..s)) + e..w <=
                   Z.of_nat
                     (if is_left (V.eq_dec e..t y)
                      then 0%nat
                      else
                       if is_left (V.eq_dec e..t x)
                       then (Z.to_nat (- n) + 1)%nat
                       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 0%nat
                         else
                          if is_left (V.eq_dec e..s x)
                          then (Z.to_nat (- n) + 1)%nat
                          else to_label (lsp G (s G) e..s)) + e..w <=
                      Z.of_nat
                        (if is_left (V.eq_dec e..t y)
                         then 0%nat
                         else
                          if is_left (V.eq_dec e..t x)
                          then (Z.to_nat (- n) + 1)%nat
                          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 -> x <> y -> VSet.In y (V G))
                           (fun (_ : ~ VSet.In e..s (V G))
                              (_ : leq_vertices G n x e..s) 
                              (_ : 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 n0))) e0
              | right n1 =>
                  (fun n2 : e..s <> y =>
                   let s1 := V.eq_dec e..t y in
                   match
                     s1 as s2
                     return
                       (Z.of_nat
                          (if is_left (right n2)
                           then 0%nat
                           else
                            if is_left (V.eq_dec e..s x)
                            then (Z.to_nat (- n) + 1)%nat
                            else to_label (lsp G (s G) e..s)) + e..w <=
                        Z.of_nat
                          (if is_left s2
                           then 0%nat
                           else
                            if is_left (V.eq_dec e..t x)
                            then (Z.to_nat (- n) + 1)%nat
                            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 n2)
                              then 0%nat
                              else
                               if is_left (V.eq_dec e..s x)
                               then (Z.to_nat (- n) + 1)%nat
                               else to_label (lsp G (s G) e..s)) + e..w <=
                           Z.of_nat
                             (if is_left (left e1)
                              then 0%nat
                              else
                               if is_left (V.eq_dec e..t x)
                               then (Z.to_nat (- n) + 1)%nat
                               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 ->
                                 x <> y -> e..s <> y -> VSet.In y (V G))
                                (fun (_ : ~ VSet.In e..t (V G))
                                   (_ : leq_vertices G n x e..t)
                                   (_ : 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 n0 n2))) e0
                   | right n3 =>
                       (fun n4 : e..t <> y =>
                        let s2 := V.eq_dec e..s x in
                        match
                          s2 as s3
                          return
                            (Z.of_nat
                               (if is_left (right n2)
                                then 0%nat
                                else
                                 if is_left s3
                                 then (Z.to_nat (- n) + 1)%nat
                                 else to_label (lsp G (s G) e..s)) + e..w <=
                             Z.of_nat
                               (if is_left (right n4)
                                then 0%nat
                                else
                                 if is_left (V.eq_dec e..t x)
                                 then (Z.to_nat (- n) + 1)%nat
                                 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 (right n2)
                                   then 0%nat
                                   else
                                    if is_left (left e1)
                                    then (Z.to_nat (- n) + 1)%nat
                                    else to_label (lsp G (s G) e..s)) + e..w <=
                                Z.of_nat
                                  (if is_left (right n4)
                                   then 0%nat
                                   else
                                    if is_left (V.eq_dec e..t x)
                                    then (Z.to_nat (- n) + 1)%nat
                                    else to_label (lsp G (s G) e..t)))
                               (Vx
                                  (eq_ind e..s
                                     (fun x : V.t =>
                                      leq_vertices G n x y ->
                                      x <> y ->
                                      lsp G x (s G) = None ->
                                      ~ VSet.In x (V G) -> VSet.In x (V G))
                                     (fun (_ : leq_vertices G n e..s y)
                                        (_ : e..s <> y)
                                        (_ : lsp G e..s (s G) = None)
                                        (_ : ~ 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 n0 Hxs Vx))) e0
                        | right n5 =>
                            (fun n6 : e..s <> x =>
                             let s3 := V.eq_dec e..t x in
                             match
                               s3 as s4
                               return
                                 (Z.of_nat
                                    (if is_left (right n2)
                                     then 0%nat
                                     else
                                      if is_left (right n6)
                                      then (Z.to_nat (- n) + 1)%nat
                                      else to_label (lsp G (s G) e..s)) +
                                  e..w <=
                                  Z.of_nat
                                    (if is_left (right n4)
                                     then 0%nat
                                     else
                                      if is_left s4
                                      then (Z.to_nat (- n) + 1)%nat
                                      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 n2)
                                        then 0%nat
                                        else
                                         if is_left (right n6)
                                         then (Z.to_nat (- n) + 1)%nat
                                         else to_label (lsp G (s G) e..s)) +
                                     e..w <=
                                     Z.of_nat
                                       (if is_left (right n4)
                                        then 0%nat
                                        else
                                         if is_left (left e1)
                                         then (Z.to_nat (- n) + 1)%nat
                                         else to_label (lsp G (s G) e..t)))
                                    (Vx
                                       (eq_ind e..t
                                          (fun x : V.t =>
                                           leq_vertices G n x y ->
                                           x <> y ->
                                           lsp G x (s G) = None ->
                                           ~ VSet.In x (V G) ->
                                           e..s <> x -> VSet.In x (V G))
                                          (fun (_ : leq_vertices G n e..t y)
                                             (_ : e..t <> y)
                                             (_ : lsp G e..t (s G) = None)
                                             (_ : ~ 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 n0 Hxs Vx n6)))
                                   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) n5
                        end) n3
                   end) n1
              end))
     : Z.of_nat
         ((fun z : V.t =>
           if is_left (V.eq_dec z y)
           then 0%nat
           else
            if is_left (V.eq_dec z x)
            then (Z.to_nat (- n) + 1)%nat
            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 0%nat
           else
            if is_left (V.eq_dec z x)
            then (Z.to_nat (- n) + 1)%nat
            else to_label (lsp G (s G) z)) y)
  ============================
   False


DEBUG:Going to execute:
clearbody XX