Inclusion preserves well-founded

Prove the following theorem (the constant inclusion is defined in module Relations).

wf_inclusion:
  forall (A:Set) (R S:A->A->Prop),
    inclusion A R S -> well_founded A S -> well_founded A R.

Solution

The solution to this exercise is given in the Coq libraries