proposition: Fact interval_dec a b i : { a <= i < b } + { i < a \/ b <= i }.
proof: Proof. destruct (le_lt_dec b i). + right; lia. + destruct (le_lt_dec a i). * left; lia. * right; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)