proposition: Lemma saturation_of_smallest r x: equivalence r -> sub x (substrate r) -> [/\ saturated r (saturation_of r x), sub x (saturation_of r x) & (forall y, sub y (substrate r) -> saturated r y -> sub x y -> sub (saturation_of r x) y)].
proof: Proof. move=> er xsr. have fc: function (canon_proj r) by fprops. split. - apply /(saturated_P4 er). by move => t /(idvalue_cprojP er xsr) [pa _]. exists (Vfs (canon_proj r) x) => //. rewrite - canon_proj_t. apply: sub_trans (f_range_graph fc); apply: dirim_Sr. - move => t tx; apply/(idvalue_cprojP er xsr); split; [by apply: xsr| ex_tac]. - move=> y ys sy sxy t. move /(idvalue_cprojP er xsr) => [tsr [z tx sc]]. move /(saturated_P3 er ys): sy => ->. by apply/(idvalue_cprojP er ys); split => //; exists z => //; apply: sxy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)