proposition: Lemma max_list_elem_of ns : ns ≠ [] → max_list ns ∈ ns.
proof: Proof. intros. induction ns as [|n ns IHns]; [done|]. simpl. destruct (Nat.max_spec n (max_list ns)) as [[? ->]|[? ->]]. - destruct ns. + simpl in *. lia. + by apply elem_of_list_further, IHns. - apply elem_of_list_here. Qed.
imports: stdpp(options)