proposition: Lemma worder_prop_eff r x (a := the_least_induced r x): worder r -> sub x (substrate r) -> nonempty x -> inc a x /\ (forall b, inc b x -> gle r a b).
proof: Proof. move => [or wor] xsr nex; move:(wor _ xsr nex) => hl. move:(iorder_osr or xsr) => [oi si]. case: (the_least_pr oi hl); rewrite si => sa sb; split => //. by move => b /sb /iorder_gle1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)