Goal:
    A : Type  size : A → nat  l : list A
  ============================
   (list_size l ≥ #|l|)


DEBUG:Going to execute:
induction l

Goals:
    A : Type  size : A → nat
  ============================
   (list_size [] ≥ #|[]|)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (list_size (a :: l) ≥ #|a :: l|)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
lia

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
Zify.zify; xlia zchecker

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
Zify.zify

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook; zify_saturate

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
intros

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
Zify.zify_pre_hook

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
idtac

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
zify_elim_let

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


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

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


DEBUG:Going to execute:
zify_op

Goals:
    A : Type  size : A → nat
  ============================
   (0 ≥ 0)

    A : Type  size : A → nat  a : A  l : list A  IHl : list_size l ≥ #|l|
  ============================
   (S (size a + list_size l) ≥ S #|l|)


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

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_iter_specs

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:
fun => <coq-core.plugins.zify::ITER@0>

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_to_euclidean_division_equations

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:
lazymatch Zify.zify_convert_to_euclidean_division_equations_flag
           with
           | true =>
               Zify.zify_internal_to_euclidean_division_equations
           | false => idtac
           end

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_convert_to_euclidean_division_equations_flag

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:
constr:(false)