proposition: Lemma sup_inf_oppP r X: order r -> sub X (substrate r) -> forall a, (least_upper_bound r X a <-> greatest_lower_bound (opp_order r) X a).
proof: Proof. move=> or Xsr a; symmetry. have [oor osr] := (opp_osr or). have Xsor: sub X (substrate (opp_order r)) by ue. move: (inf_sup_oppP oor Xsor a). by rewrite /opp_order (igraph_involutive (proj41 or)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)