proposition: Fact nat_sorted_injective ll : nat_sorted ll -> list_injective ll.
proof: Proof. intros H l a m b r E; generalize (H _ _ _ _ _ E); lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)