proposition: Fact nat_rev_bounded_ind x y : x <= y <= k -> P y -> P x.
proof: Proof. Proof using HP. intros H1 H2. refine (proj1 (@nat_rev_ind (fun n => P n /\ n <= k) _ x y _ _)). clear x y H1 H2; intros n (H1 & H2); split; auto; lia. lia. split; auto; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)