proposition: Lemma saturated_P4 r x: equivalence r -> sub x (substrate r) -> (saturated r x <-> (exists2 b, sub b (quotient r) & x = Vfs (inverse_fun (canon_proj r)) b)).
proof: Proof. move=> er xs. have qr: quotient r = target (canon_proj r) by aw. have sj := (canon_proj_fs er). split. move/(saturated_P3 er xs) => hyp. exists (Vfs (canon_proj r) x) =>//. rewrite qr;apply: sub_trans (f_range_graph (proj1 sj)); apply: dirim_Sr. move=> [b bq xeq]. apply/(saturated_P3 er xs). rewrite qr in bq; move: (direct_inv_im_surjective sj bq). by rewrite /inverse_direct_value -xeq => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)