proposition: Fact nat_sinc_inj f a b : (forall x y, a <= x < y /\ y <= b -> f x < f y) -> (forall x y, a <= x <= b -> a <= y <= b -> f x = f y -> x = y).
proof: Proof. intros H0 x y Hx Hy. destruct Hx; destruct Hy. destruct (lt_eq_lt_dec x y) as [ [ ? | ? ] | ? ]; auto. specialize (H0 x y). spec in H0; repeat split; auto; intro; lia. specialize (H0 y x). spec in H0; repeat split; auto; intro; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)