proposition: Lemma list_max_app : forall l1 l2, list_max (l1 ++ l2) = max (list_max l1) (list_max l2).
proof: Proof. intro l1; induction l1 as [|a l1 IHl1]; intros l2; [ reflexivity | ]. now simpl; rewrite IHl1, Nat.max_assoc. Qed.
imports: PeanoNat