This fact is already proved in Coq.Wellfounded.Inclusion, but I like
this formulation better: the hypotheses are reversed, which makes the
lemma easier to use.
Lemma well_founded_inclusion:
forall {
A :
Type } {
lt1 lt2 :
A ->
A ->
Prop },
well_founded lt1 ->
(
forall a1 a2,
lt2 a1 a2 ->
lt1 a1 a2) ->
well_founded lt2.
Proof.
unfold well_founded; intros ? ? ? h ?; intro a.
generalize a (h a). clear h a.
induction 1. constructor. eauto.
Qed.