proposition: Lemma cofinal_right_directed r A: right_directed r -> cofinal r A -> right_directed (induced_order r A).
proof: Proof. move/right_directedP => [or rr] [As co]; apply /right_directedP. have [pa pb] := (iorder_osr or As). split; [ exact | hnf; rewrite pb]. move=> x y xA yA; move: (rr _ _ (As _ xA)(As _ yA)) => [z [xz yz]]. move:(co _ (arg2_sr xz))=> [t tA tz]. exists t; split; apply/iorder_gle0P => // ;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)