未解決問題_list_max.v

Require Import Arith List.
Import ListNotations.

Definition list_reduce_left {A: Type} (f: A -> A -> A) (xs: list A) :=
  match xs with
  | [] => None
  | x :: xs =>
    Some (List.fold_left f xs x)
  end.

Definition list_max {A: Type} max (xs: list A) := list_reduce_left max xs.

Lemma list_max_Forall_nat : forall xs x,
    list_max max xs = Some x ->
    List.Forall (fun y => y <= x) xs.
Proof.
  (*未解決*)
Admitted.