proposition: Lemma least_left_directed r: order r -> has_least r -> left_directed r.
proof: Proof. move=> or [a [asr ga]]; apply /left_directedP. by split =>//; move=> x y xr yr; exists a; split; apply:ga. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)