proposition: Lemma sub_right_directed_trans J J' r: preorder r -> sub_right_directed J r -> sub_right_directed J' (induced_order r J) -> sub_right_directed J' r.
proof: Proof. move => or [ha hb][hc hd]; rewrite (ipreorder_sr or ha) in hc. split => //. by apply: (sub_trans hc ha). move => i j iI jI. by move:(hd i j iI jI) => [z [za /iorder_gle1 zb /iorder_gle1 zc]]; exists z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)