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