proposition: Lemma sub_part_relsetX y x: partition_s y x -> sub (partition_relset y x) (coarse x).
proof: Proof. move=> pa; rewrite partition_relset_pr // => t tu. by move: (setU_hi tu) => [z tz /Zo_P [/setP_P zp _ ]]; apply: zp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)