proposition: Theorem nat_rev_ind' x y : x <= y <= k -> P y -> P x.
proof: Proof. Proof using HP. intros H1 H2. set (Q n := n <= k /\ P n). assert (forall x y, x <= y -> Q y -> Q x) as H. apply nat_rev_ind. intros n (H3 & H4); split. lia. revert H4; apply HP, H3. apply (H x y). lia. split; auto; lia. Qed.
imports: Arith Lia