proposition: Lemma least_opposite a r: order r -> least r a -> greatest (opp_order r) a.
proof: Proof. by move=> /opp_osr [_ pb] [asr hy]; split; rewrite pb // => x /hy /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)