proposition: Lemma right_directed_ind_prop r J: preorder r -> sub J (substrate r) -> right_directed_on r J -> right_directed_on (induced_order r J) J.
proof: Proof. move => or sr rdr x y xJ yJ. move:(rdr _ _ xJ yJ) => [z [zJ za zb]]; exists z. by split=> //;apply/iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)