proposition: Lemma inf_sup_opp r X: order r -> sub X (substrate r) -> has_infimum r X -> (has_supremum (opp_order r) X /\ supremum (opp_order r) X = infimum r X).
proof: Proof. move => or sa sb. have hh:= (proj1 (opp_osr or)). move: (infimum_pr1 or sb) => sc. move /(inf_sup_oppP or sa): sc => w. by split; [ exists (infimum r X) | symmetry; apply: supremum_pr2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)