proposition: Lemma infimum_pr X r: order r -> sub X (substrate r) -> has_infimum r X -> (lower_bound r X (infimum r X) /\ forall z, lower_bound r X z -> gle r z (infimum r X)).
proof: Proof. by move=> or Xsr /(infimum_pr1 or) /(glbP or Xsr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)