proposition: Lemma saturation_of_pr r x: equivalence r -> sub x (substrate r) -> saturation_of r x = union (Zo (quotient r)(fun z=> exists2 i, inc i x & z = class r i)).
proof: Proof. move=> er sr. have fc: function (canon_proj r) by fprops. rewrite /saturation_of/inverse_direct_value. set_extens y. move /(idvalue_cprojP er sr) => [v [pa pb pc]]. apply: (@setU_i _ (class r y)); fprops; apply: Zo_i; fprops. by ex_tac; rewrite pd. move /setU_P => [z zy/Zo_P [zq [i ix sc]]]. move: zy; rewrite sc; move/(class_P er) => pc. apply/(idvalue_cprojP er sr); split;first by substr_tac. ex_tac;symmetry;by apply:class_eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)