Goal:
  
  a : Nbar.t
  l : list Nbar.t
  IHl : forall acc : Nbar.t,
        (Some 0 <= acc)%nbar -> (Some 0 <= fold_left max l acc)%nbar
  acc : Nbar.t
  H : (Some 0 <= acc)%nbar
  ============================
   ((Some 0 <= acc)%nbar \/ (Some 0 <= a)%nbar)


DEBUG:Going to execute:
now left
DEBUG LTAC Evaluated term: max_le'