Goal:
    n : Z  l : list Z
  ============================
   (forall m : Z, n <= m \/ Exists (Z.le n) l -> n <= fold_left Z.max l m)


DEBUG:Going to execute:
induction l

Goals:
    n : Z
  ============================
   (forall m : Z, n <= m \/ Exists (Z.le n) [] -> n <= fold_left Z.max [] m)

  
  n : Z
  a : Z
  l : list Z
  IHl : forall m : Z, n <= m \/ Exists (Z.le n) l -> n <= fold_left Z.max l m
  ============================
   (forall m : Z,
    n <= m \/ Exists (Z.le n) (a :: l) -> n <= fold_left Z.max (a :: l) m)


DEBUG:Going to execute:
cbn in *
DEBUG LTAC Evaluated term: l

Goals:
    n : Z
  ============================
   (forall m : Z, n <= m \/ Exists (Z.le n) [] -> n <= m)

  
  n : Z
  a : Z
  l : list Z
  IHl : forall m : Z, n <= m \/ Exists (Z.le n) l -> n <= fold_left Z.max l m
  ============================
   (forall m : Z,
    n <= m \/ Exists (Z.le n) (a :: l) -> n <= fold_left Z.max l (Z.max m a))


DEBUG:Going to execute:
intros m [H| H]