proposition: Lemma coarser_preorder_gleP1 x u v: gle (coarser_preorder x) u v <-> [/\ preorder u, preorder v, substrate u = x, substrate v = x & forall a b, inc a x -> inc b x -> related u a b -> related v a b].
proof: Proof. split. move/coarser_preorder_gleP => [pu pv su sv hyp]; split => //. by move=> a b ax bx J1; apply: hyp. move => [pu pv su sv hyp]. apply /coarser_preorder_gleP; split => // t tu. have p:= (preorder_sgraph pu tu). rewrite -p in tu |- *; apply: hyp =>//; rewrite - su; substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)