proposition: Lemma Exercise1_3a5P x y (f := fam_of_substrates g) : related (partition_relation (disjointU_function f) (disjointU f)) x y <-> [/\ inc x E13_sF, inc y E13_sF & Q x = Q y].
proof: Proof. move: (disjointU_function_pr f) => [p1 p2]. have p3:partition_w_fam (graph (disjointU_function f)) (disjointU f). rewrite p2; apply: partition_disjointU; apply: fos_graph. apply: (iff_trans (isc_rel_P p1 p3 x y)). rewrite /in_same_coset/Vf/disjointU/disjointU_function; aw. rewrite /disjointU_fam; split. move=> [i [idf]]; rewrite LgV// => /indexed_P [px pxv qx] /indexed_P [py pyv qy]. rewrite qx qy -px -py; split => //; apply: disjointU_pi; ue. have ->: domain f = domain g by rewrite /f/fam_of_substrates; aw. move=> [xsg ysg sq]. move: (du_index_pr1 xsg) (du_index_pr1 ysg)=> [qxd pxs px][_ pys py]. exists (Q x); rewrite /f /fam_of_substrates ! LgV//. split => //;apply /indexed_P; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)