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