proposition: Fact list_upper_bound (l : list nat) : { m | forall x, In x l -> x < m }.
proof: Proof. induction l as [ | x l (m & Hm) ]. + exists 0; simpl; tauto. + exists (1+x+m); intros y [ [] | H ]; simpl; try lia. generalize (Hm _ H); intros; lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)