proposition: Lemma part_relset_anti x y y': partition_s y x -> partition_s y' x -> (partition_relset y' x = partition_relset y x) -> y = y'.
proof: Proof. move: x y y'. suff: (forall x y y', partition_s y x -> partition_s y' x -> (partition_relset y' x = partition_relset y x) -> sub y y'). move=> aux a b c p1 p2 eq; apply: extensionality. apply: aux p1 p2 eq. apply: aux p2 p1 (sym_eq eq). move=> x y y' pa pa'. rewrite (partition_relset_pr pa) (partition_relset_pr pa') => eq a ay. have cpy:= (partition_relset_pr1 pa ay). have [b ba] := (proj2 pa _ ay). have p: (forall u v,inc u a -> inc v a -> exists c, [/\ inc c y', inc u c & inc v c]). move=> u v ua va. have p1: inc (J u v) (coarse a) by apply:setXp_i. have p2: (inc (J u v) (union (partition_relset_aux y' x))). rewrite eq; union_tac. have [z Jbb /Zo_P [zp [c cy zc]]] := (setU_hi p2). by exists c; split=> //; move: Jbb; rewrite zc; move/setXp_P => []. have [c [cy bc _]] := (p _ _ ba ba). suff: a = c by move=> ->. set_extens t => ta. have [c' [cy' tc' _]] := (p _ _ ta ta). have [c'' [cy'' bc'' tc'']] := (p _ _ ba ta). case:((proj2 (proj1 pa') )_ _ cy cy''). move => ->; case:((proj2 (proj1 pa')) _ _ cy'' cy'); first by move => ->. by move=> dcf;case: (nondisjoint tc'' tc' dcf). by move=> dcf;case: (nondisjoint bc bc'' dcf). have p1: (inc (J b t) (coarse c)) by apply:setXp_i. have p2: (inc (J b t) (union (partition_relset_aux y' x))). apply: (setU_i p1); apply: (partition_relset_pr1 pa' cy). move: p2; rewrite eq /partition_relset_aux => p2. have [z Jbb /Zo_P [zp [d dy zx]]]:= (setU_hi p2). move: Jbb; rewrite zx; move/setXp_P => [bd td]. case:((proj2 (proj1 pa)) _ _ ay dy); first by move=> ->. move=> dfc; case: (nondisjoint ba bd dfc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)