proposition: Lemma partition_relset_order x y y': partition_s y x -> partition_s y' x -> (sub (partition_relset y' x)(partition_relset y x) <-> gle (coarser x) y y').
proof: Proof. move=> pa pa'. do 2 rewrite partition_relset_pr //. split; last first. move /coarser_gleP=> [_ _ hyp] z /setU_hi [t zt /Zo_P [tp [a ay tc]]]. have [b iby ab] := (hyp _ ay). apply: (@setU_i _ (coarse b)); first by apply (setX_Sll ab); ue. by apply: partition_relset_pr1. move => suu; apply/coarser_gleP;split=>// a ay. have [b ba]:=(proj2 pa' _ ay). have p: (forall u, inc u a -> exists c, [/\ inc c y, inc b c& inc u c]). move=> u ua. have q: (inc (J b u) (union (partition_relset_aux y' x))). apply: (@setU_i _ (coarse a)); first by apply:setXp_i. apply: (partition_relset_pr1 pa' ay). have [z Jbb /Zo_P [zp [c cy zc]]] := (setU_hi (suu _ q)). by move: Jbb; rewrite zc; move/setXp_P=> [s1 s2]; exists c. move: (p _ ba) => [c [cy bc _]]; ex_tac => d /p [f [fy bf df]]. case: (proj2 (proj1 pa) _ _ cy fy); first by move => ->. by move=> dcf; case: (nondisjoint bc bf dcf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)