proposition: Lemma intersection_is_partition f x: fgraph f -> (allf f (partition_s ^~ x)) -> nonempty (domain f) -> partition_s (intersection_partition f) x.
proof: Proof. move=> fgf alp nedf; move: (nedf) => [w wdf]. split; last by move=> a /setC1_P [_] /nonemptyP. rewrite /intersection_partition; split. set_extens t. move=> /setU_P [y ty] /setC1_P [] /funI_P [z zp h] _. move: (alp _ wdf) => [[pu1 pu3] pu2]. move: zp => /setXb_P [fgz df VV]; rewrite -df in wdf. have aux: inc t (Vg z w) by rewrite h in ty; apply: (setIb_hi ty wdf). rewrite -pu1; apply /setU_P; exists (Vg z w) => //; apply: VV; ue. move => tx; apply /setU_P. pose g u := select (inc t) (Vg f u). have gp u: inc u (domain f) -> inc t (g u) /\ inc (g u) (Vg f u). move=> udf; move:(alp _ udf) tx =>[[<- aa] bb] /setU_P [z z1 z2]. apply: select_pr; [ ex_tac | move => v1 v2 ha hb hc hd]. move: (aa v1 v2 ha hc); case => //; rewrite /disjoint=> dd; empty_tac1 t. set (h:= Lg (domain f) g). have tih:(inc t (intersectionb h)). apply: setIb_i. exists (J w (Vg h w)); apply: fdomain_pr1; rewrite /h; aww. move=> i; rewrite /h Lgd => idf; move: (gp _ idf) => [res _]; rewrite LgV//. have hp:(inc h (productb f)). apply /setXb_P; rewrite /h;aw; split;fprops;move=> i idf; rewrite LgV//. exact: (proj2(gp _ idf)). exists (intersectionb h) => //; apply /setC1_P; split. apply /funI_P;ex_tac. move=> he; move: tih; rewrite he; case/in_set0. move => a b /setC1_P [] /funI_P [z1 z1p] -> _ /setC1_P [] /funI_P [z2 z2p] -> _. apply: disjoint_pr1 => y yi1 yi2. move: z1p z2p => /setXb_P [fg1 dz1 VV1] /setXb_P [fg2 dz2 VV2]. apply: f_equal; apply: fgraph_exten => //; [ue | move=> i idf /=]. rewrite -dz1 in VV1. move: (VV1 _ idf)(setIb_hi yi1 idf) => p1 p2. rewrite -dz2 in VV2; rewrite dz1 -dz2 in idf. move: (VV2 _ idf) (setIb_hi yi2 idf)=> p3 p4. rewrite dz2 in idf. case:(proj2 (proj1 (alp _ idf)) _ _ p1 p3) => // di; empty_tac1 y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)