proposition: Lemma max_of_list_app l l' : max_of_list (l ++ l') = max (max_of_list l) (max_of_list l').
proof: Proof. by induction l; ins; rewrite IHl, Max.max_assoc. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation