Saturating the proof context using a lemma

When I write tactics, I often want to saturate the proof context using a particular lemma. A typical example would be adding to the proof context all the inequalities a <= b that I can obtain by transitivity.

Ltac saturate_le :=
  repeat
  (match goal with
     | [ H : ?a <= ?b, H' : ?b <= ?c |- _ ] => progress (
       match goal with
         | [ G : a <= c |- _ ] => idtac
         | [ |- _ ] => assert (a <= c) by
               (apply (Nat.le_trans a b c H H'))
       end)
  end).

Lemma long_trans : forall a b c d, a <= b -> b <= c -> c <= d -> a <= d.
Proof.
  intros.
  saturate_le.
  assumption.
Qed.

My saturate_le tactic is a bit convoluted because I need to make sure I am not adding a statement that I already know.

Is there a generic way to define such a tactic, that would close the context under a list of fairly arbitrary lemmas?