proposition: Lemma or_cut_segment r x : order r -> or_cut r (Zo (substrate r) (fun t => glt r x t)).
proof: Proof. move => or;split; first by apply:Zo_S. move => a b /Zo_P[_ lxa lab]; apply/Zo_P; split; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)