Goal:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  ============================
   (None <= Some (nxy2 - 1)%Z)%nbar


DEBUG:Going to execute:
trivial; hnf; intros; (solve
            [ do
            ![ solve
             [ trivial | apply : eq_sym ; trivial ]
             | discriminate
             | contradiction
             | Ltac.split ]
            | case not_locked_false_eq_true; Ltac.assumption
            | match goal with
              | H:~ _ |- _ => solve [ case H; trivial ]
              end ])