proposition: Theorem nat_sorted_rect l : nat_sorted l -> P l.
proof: Proof. Proof using HP0 HP1 HP2. induction l as [ [ | x [ | y l ] ] IHl ] using (measure_rect (@length _)). intro; apply HP0. intro; apply HP1. intros H; apply HP2. revert H; apply nat_sorted_head_inv. apply IHl. rew length; lia. revert H; apply nat_sorted_cons_inv. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)