proposition: Lemma cofinal_directed S J: cofinal (isr S) J -> sub_right_directed J (isr S).
proof: Proof. move => [pa pb]; split => // i j iI jI. rewrite is_substrate_r in pa. move: (is_directed_r (pa _ iI) (pa _ jI)) => [z [zI za zb]]. move:(pb _ (arg2_sr za)) => [t tI tm]. by exists t; split => //; apply:(proj33 (is_preorder_r S)) tm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)