proposition: Lemma lmaxSpec : forall (l : list nat), lforall (fun n=> n <= lmax l) l.
proof: Proof. intros. apply lForallSame. induction l; cpx. allsimpl. dands; cpx. - apply Max.le_max_l. - apply lForallSame. apply lForallSame in IHl. eapply implies_lforall; eauto. introv H Hlt; allsimpl; cpx. apply Nat.max_le_compat_l with (p:= a) in Hlt. pose proof (Max.le_max_r a a0). omega. Qed.
imports: AssociationList Omega variables String Ascii