proposition: Lemma partition_relset_pr y x: partition_s y x -> partition_relset y x = union (partition_relset_aux y x).
proof: Proof. move=> pa. have pfa: (partition_w_fam (graph(part_fun y x)) x) by apply: pfs_partition. have sp:source (part_fun y x) = y by rewrite /part_fun /canonical_injection;aw. move: (partition_set_in_PP pa); aw => ypp. have p1: function (part_fun y x) by apply: pfs_f. have p2: partition_w_fam (graph (part_fun y x)) x. by move: (prs_is_equivalence pa); fprops. have p3: sgraph (partition_relation (part_fun y x) x). by rewrite /partition_relation; apply: graph_on_graph. have p4:sgraph (union (partition_relset_aux y x)). move=> t tp; move: (setU_hi tp); rewrite/partition_relset_aux. by move=> [z tz /Zo_P [] /setP_P zp _]; move: (zp _ tz) => /setX_P []. apply: sgraph_exten => //. move=> u v; split. move /(isc_rel_P p1 p2); rewrite /in_same_coset sp. move=> [i [iy ]]; rewrite pfs_V // => ui vi. apply (@setU_i _ (coarse i)); first by apply: setXp_i. by apply: partition_relset_pr1. move/setU_P => [z pz] /Zo_P [zp [a ay zc]]. move: pz; rewrite zc; move /setXp_P => [ua va]. by apply/(isc_rel_P p1 p2); hnf;rewrite sp; exists a;split=> //; rewrite pfs_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)