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


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| reflexivity
| symmetry; trivial
| contradiction
| congruence ]