proposition: Lemma preordersP x z: inc z (preorders x) <-> (preorder_on z x).
proof: Proof. split; first by move/Zo_P => []. move => h;apply:Zo_i => //;apply/setP_P. by move: h => [pa <-]; apply:sub_graph_coarse_substrate; apply: preorder_sgraph. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)