proposition: Lemma olexp_total: total_order olexp.
proof: Proof. move: olexp_osr => [oo so]; split => //. have atg: (allf olexp_g total_order). by rewrite /olexp_g/cst_graph; red; aw => i isr; rewrite LgV//; apply: worder_total. move: (olex_cc_comparable1 olexp_ax atg) => pa. rewrite -/olexp' in pa. move=> x y xE yE. have xe: inc x (prod_of_substrates olexp_g). move: xE; rewrite so => xe; move: (olexp_Gs xe). rewrite - (olex_sr (opp_order r')) //. have ye: inc y (prod_of_substrates olexp_g). move: yE; rewrite so => ye; move: (olexp_Gs ye). rewrite - (olex_sr (opp_order r')) //. move: xE yE; rewrite so => xsr ysr. move: (olexp_Gxy1 xsr ysr) => wor''. have: (gle olexp' x y \/ gle olexp' y x). by move: (pa x y); rewrite /ocomparable; move => ->; rewrite /olexp' olex_sr. by case => h; [left | right ]; apply /iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)