proposition: Lemma infimum_pr1 X r: order r -> has_infimum r X -> greatest_lower_bound r X (infimum r X).
proof: Proof. move => or [z h]. apply: the_greatest_pr => //; last by exists z. exact: (proj1 (iorder_osr or (Zo_S(p:=lower_bound r X)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)