I have tried to make a function in Coq which has a pretty complex termination argument. To make it easier, I am able to write the function so that it has a natural number as first argument, so that either the number or the argument after it is structurally smaller.

When trying the nested fix approach to recursion on two arguments, Coq complains that a proof argument that contains the semantics of the decreasing number is not an inductive type.

I could probably do well-founded recursion manually, but I would like to use Program Fixpoint or Equations. With Program Fixpoint I get a very ugly version of the well-foundedness proof. Below is a minimal code example that demonstrates the ugliness.

```
Require Import Program Omega.
Inductive tuple_lt : (nat * nat) -> (nat * nat) -> Prop :=
fst_lt : forall a b c d, a < c -> tuple_lt (a, b) (c, d).
Program Fixpoint f (a : nat) (b : nat) {measure (a, b) (tuple_lt)} :=
match a with
| 0 => 0
| S n => f n b
end.
Next Obligation.
apply fst_lt. auto.
Qed.
Next Obligation.
unfold well_founded. unfold MR.
```

The obligation looks like this:

```
forall a : {_ : nat & nat}, Acc (fun x y : {_ : nat & nat} => tuple_lt (projT1 x, projT2 x) (projT1 y, projT2 y)) a
```

Can I somehow transform a proof of `Acc tuple_lt`

into that ugly proof or avoid generating it?

Is there a proof in the standard library for structural recursion on two arguments?

How do I even write a manual WF proof using Equations? The manual does not mention that.