proposition: Lemma total_order_opposite r: total_order r -> total_order (opp_order r).
proof: Proof. move=> [or tor]; hnf; move: (opp_osr or) => [oo ->]; split => // x y xs ys. by case: (tor _ _ xs ys)=> h; [right |left]; apply/igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)