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