proposition: Lemma olexp_lEp: nonempty (substrate r) -> (inc olexp_lE (substrate r) /\ (forall x, inc x (substrate r) -> gle r olexp_lE x)).
proof: Proof. have or: order r by move: wor => [or _]. move => ne; move: (the_least_pr or (worder_least wor ne)). by rewrite -/olexp_lE; move=> [pa pb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)