proposition: Lemma olexp_G_least (m:= cst_graph (substrate r') olexp_lE): nonempty (substrate r) -> least olexp m.
proof: Proof. move=> nsr. have mp: inc m (substrate olexp). rewrite (proj2 olexp_osr); apply: Zo_i. move: (olexp_lEp nsr) => [pc _]. apply /gfunctions_P2; rewrite /m /cst_graph; split;aww. by move=> u /Lg_range_P [b bsr ->]. have ->: olexp_I m = emptyset. apply /set0_P => t /Zo_P [pa pb]; case: pb. rewrite /m /cst_graph LgV//. apply: emptyset_finite. split => // x xsr. move: olexp_total => tor; case: (total_order_pr2 tor xsr mp) => cp //. move: cp => [] /olexp_gleP [pa pb pc] xm. case: pc; first by contradiction. move=> [j [jsr cp1 _]]; move: cp1; rewrite /m /cst_graph LgV// => lt1. have or: order r by move: wor => []. have vsr: inc (Vg x j) (substrate r) by order_tac. move: (olexp_lEp nsr) => [_ h]; move: (h _ vsr) => le1; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)