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