proposition: Lemma list_max_le : forall l n, list_max l <= n <-> Forall (fun k => k <= n) l.
proof: Proof. intro l; induction l as [|a l IHl]; simpl; intros n; split. - now intros. - intros. now apply Nat.le_0_l. - intros [? ?] %Nat.max_lub_iff. now constructor; [|apply IHl]. - now rewrite Forall_cons_iff, <- IHl, Nat.max_lub_iff. Qed.
imports: PeanoNat