proposition: Lemma inc_infimum_substrate X r: order r -> sub X (substrate r) -> has_infimum r X -> inc (infimum r X) (substrate r).
proof: Proof. move=> or Xsr hs. by move: (infimum_pr1 or hs)=> /(glbP or Xsr) [[aa _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)