proposition: Lemma ordersP x z: inc z (orders x) <-> (order_on z x).
proof: Proof. split; [by move /Zo_hi | move => h; apply: Zo_i => //]. apply /setP_P; move: h => [or <-]. apply: sub_graph_coarse_substrate; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)