proposition: Lemma worder_prop2 r (p:property): worder r -> (forall x, inc x (substrate r) -> p x) \/ (exists x, [/\ inc x (substrate r), ~p x & forall y, glt r y x -> p y]).
proof: Proof. move => wor; set A := Zo (substrate r) (fun x => ~p x). case: (emptyset_dichot A) => aE. by left; move => x xst; ex_middle bad;empty_tac1 x; apply: Zo_i. right. have sar: sub A (substrate r) by apply: Zo_S. move: (worder_prop wor sar aE) =>[x /Zo_P[csr xa] xp]; exists x. split => // => y lxy; ex_middle bad. have /xp la: inc y A by apply: Zo_i => //; apply: (arg1_sr (proj1 lxy)). case: (not_le_gt (proj1 wor) la lxy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)