proposition: Lemma partition_relset_pr1 y x a: partition_s y x -> inc a y -> inc (coarse a) (partition_relset_aux y x).
proof: Proof. move=> pa ay. move /setP_P: (partition_set_in_PP pa) => yp. apply:Zo_i; last by ex_tac. by apply /setP_P; apply:setX_Sll; apply/setP_P; apply: yp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)