proposition: Lemma section_is_representative_system_function g f x: function f -> partition_w_fam (graph f) x -> is_right_inverse (canon_proj (partition_relation f x)) g -> (forall u, inc u (source f) -> nonempty (Vf f u)) -> representative_system_function g f x.
proof: Proof. move=> ff pf ti alne. have ig: injection g by apply: (right_inverse_fi ti). apply: rep_sys_function_pr2=>//. rewrite - (proj33 (proj1 ti)) canon_proj_s isc_rel_sr; fprops. move=> i isf. set (r:=partition_relation f x) in *. have sf: domain (graph f) =source f by apply: domain_fg. have er: equivalence r by rewrite /r; apply: isc_rel_equivalence. have sr: substrate r = x by rewrite /r isc_rel_sr. rewrite (right_i_source ti); aw. apply /unique_existence;split. set z:= (rep (Vf f i)). have zW: inc z (Vf f i) by rewrite /z; apply: rep_i; apply: alne. have zx: inc z x by move: pf=>[_ md <-]; rewrite - sf in isf; union_tac. exists (class r z); split. aw; rewrite - sr in zx; fprops. move: (section_canon_proj_pr (refl_equal r) ff pf ti zx). move /(isc_rel_P ff pf) => [ u [usf zW' qW]]. by rewrite (partition_inc_unique1 ff pf isf zW usf zW'). aw; move=> a b [atx Wa] [btx Wb]. have Wiq: inc (Vf f i) (quotient r). apply/(setQ_P er); apply (isc_rel_class2 ff pf isf); ex_tac. have aux: (forall u, inc u (quotient r) -> inc (Vf g u) (Vf f i) -> Vf f i = u). move=> u /(setQ_P er) [rs eq] iWW; rewrite sr in rs. rewrite eq; apply: is_class_pr=> //. move: (section_canon_proj_pr (refl_equal r) ff pf ti rs). rewrite - eq; move /(isc_rel_P ff pf) => [v [usf zW' qW]]. by rewrite (partition_inc_unique1 ff pf isf iWW usf qW). by rewrite -(aux _ atx Wa) (aux _ btx Wb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)