proposition: Lemma supremum_singleton r x: order r -> inc x (substrate r) -> supremum r (singleton x) = x.
proof: Proof. by move=> or xsr; apply: sup_comparable1=> //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)