proposition: Lemma pfs_partition p E: partition_s p E -> partition_w_fam (graph (part_fun p E)) E.
proof: Proof. move=> pa. move: (pfs_f pa) => fpa. move: (pa)=> [[ux di] _]. have Wp i: inc i p -> Vg (graph (part_fun p E)) i = i. by move => iy; apply: pfs_V. have dg: domain (graph (part_fun p E)) = p. by rewrite domain_fg // /part_fun /canonical_injection; aw. split; fprops. by move=> i j; rewrite dg => iy jy; rewrite Wp // Wp //; apply: di. set_extens v => vs. move: (setUb_hi vs)=> [w]; rewrite dg. move=> wy; rewrite Wp // -ux => vW; union_tac. rewrite -ux in vs; move: (setU_hi vs) => [w vw wy]. by apply /setUb_P; exists w; rewrite ? dg ? (Wp _ wy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)