proposition: Lemma coarse_related u x y: related (coarse u) x y <-> (inc x u /\ inc y u).
proof: Proof. by split; [ move/setX_P => [_]; aw | move => [pa pb];apply : setXp_i ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)