proposition: Lemma infimum_pr2 r X a: order r -> greatest_lower_bound r X a -> a = infimum r X.
proof: Proof. move=> or le. have hs: has_infimum r X by exists a. exact: (infimum_unique or le (infimum_pr1 or hs)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)