proposition: Lemma worder_prop_rev r: order r -> (forall x, sub x (substrate r) -> nonempty x -> exists2 a, inc a x & (forall b, inc b x -> gle r a b)) -> worder r.
proof: Proof. move => h1 h2; split => // x xsr nex; move: (h2 x xsr nex) => [a ax ap]. exists a; hnf; rewrite iorder_sr //;split => // b bx. by apply/iorder_gle0P => //; apply: ap. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)