proposition: Lemma inc_supremum_substrate X r: order r -> sub X (substrate r) -> has_supremum r X -> inc (supremum r X) (substrate r).
proof: Proof. move=> or Xsr hs. by move: (supremum_pr1 or hs)=> /(lubP or Xsr) [[aa _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)