proposition: Theorem left_directed_minimal r x: left_directed r -> minimal r x -> least r x.
proof: Proof. move=> rr [xsr ma]; split=>// t ts. move/left_directedP: rr => [or rr]. by move:(rr _ _ xsr ts) => [z [xz tz]];rewrite - (ma _ xz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)