proposition: Lemma olexp_ax: olex_ax (opp_order r') olexp_g.
proof: Proof. have or': order r' by move: wor' => [ok _]. split => //. by apply total_order_opposite; apply worder_total. by rewrite (proj2 (opp_osr or')) /olexp_g /cst_graph; aw. by rewrite /olexp_g; hnf;aw;move => x xsr; rewrite LgV//; move: wor => [or _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)