proposition: Lemma section_canon_proj_pr g f x y r: r = partition_relation f x -> function f -> partition_w_fam (graph f) x -> is_right_inverse (canon_proj r) g -> inc y x -> related r y (Vf g (class r y)).
proof: Proof. move=> pr ff pf ri yx. have eq: equivalence r by rewrite pr; apply: isc_rel_equivalence. have sr: substrate r = x by rewrite pr isc_rel_sr //. rewrite - sr in yx. have cyq: inc (class r y) (quotient r) by fprops. have sg: source g = target (canon_proj r) by apply: right_i_source. move: sg; aw => sg; rewrite - sg in cyq. have yri: inc y (class r y) by apply: inc_itself_class => //. apply: (symmetricity_e eq). apply /(class_P eq). have <- //: (class r y) = class r (Vf g (class r y)). have [pa pb] := ri. set t := (class r y). have Wcs: inc (Vf g t) (substrate r) by move: pa=> [_ fg]; aw; move=>->; Wtac. move: (compfV pa cyq). rewrite pb idV // ? canon_proj_V //; aw; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)