proposition: Lemma inf_sup_oppP r X: order r -> sub X (substrate r) -> forall a, (greatest_lower_bound r X a <-> least_upper_bound (opp_order r) X a).
proof: Proof. move=> or Xsr a. have [oor osr] := (opp_osr or). have Xsor: sub X (substrate (opp_order r)) by ue. apply:(iff_trans (glbP or Xsr a)); symmetry; apply:(iff_trans(lubP oor Xsor a)). by split; move => [pa pb]; split; try (apply /(opposite_lower_boundP or) => //); move => z /(opposite_lower_boundP or) => h; apply/igraph_pP; apply: pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)