Lack of sub_trans in ssrbool.v

[hoheinzollern]

Looking at the file ssrbool.v and lemmas related to sub_mem, I was a bit surprised not to find a lemma of this shape:

Lemma sub_trans T (mp mq mr : mem_pred T) :
  sub_mem mp mq -> sub_mem mq mr -> sub_mem mp mr.
Proof. by move=> pq qr x /pq /qr. Qed.

Is there a rationale why this lemma is not there? I could not find one and I could prove what I wanted (math-comp/math-comp#1380) easily without it.

I'm curious at this point to know whether the lack of this lemma is intentional.