Decreasing analysis

[Rocq] A termination check in Rocq that verifies recursive functions always call themselves on structurally smaller arguments, ensuring all computations terminate (required for logical consistency).