proposition: Lemma worder_prop r x: worder r -> sub x (substrate r) -> nonempty x -> exists2 a, inc a x & (forall b, inc b x -> gle r a b).
proof: Proof. move => [or wor] xsr nex; move:(wor _ xsr nex) => [a []]; rewrite iorder_sr //. by move=> ax ap; ex_tac => b /ap /iorder_gle1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)