Goal:
  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
idtac

Goals:
    A : Type  size : A → nat
  ============================
   (BinInt.Z.ge BinNums.Z0 BinNums.Z0)

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
Zify.zify_post_hook

Goals:
    A : Type  size : A → nat
  ============================
   (BinInt.Z.ge BinNums.Z0 BinNums.Z0)

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
idtac

Goals:
    A : Type  size : A → nat
  ============================
   (BinInt.Z.ge BinNums.Z0 BinNums.Z0)

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
zify_saturate

Goals:
    A : Type  size : A → nat
  ============================
   (BinInt.Z.ge BinNums.Z0 BinNums.Z0)

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@1>

Goals:
    A : Type  size : A → nat
  ============================
   (BinInt.Z.ge BinNums.Z0 BinNums.Z0)

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
xlia zchecker

Goals:
    A : Type  size : A → nat
  ============================
   (BinInt.Z.ge BinNums.Z0 BinNums.Z0)

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.ge (BinInt.Z.of_nat (list_size l)) (BinInt.Z.of_nat #|l|)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.ge
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))
      (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
<coq-core.plugins.micromega::Lia@0> $1