proposition: Lemma opposite_upper_boundP r: order r -> forall X x, (upper_bound r X x <-> lower_bound (opp_order r) X x).
proof: Proof. rewrite /upper_bound/lower_bound=> or X; rewrite (proj2 (opp_osr or)). by split; move=> [xsr h]; split=>//; move=> y yR; move:(h _ yR); move/igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)