proposition: Lemma saturated_setC r a: equivalence r -> sub a (substrate r) -> saturated r a -> saturated r ((substrate r) -s a).
proof: Proof. move=> er ar. move /(saturated_P4 er ar) => [b sq aib]. apply /(saturated_P4 er);first by apply: sub_setC. exists ((quotient r) -s b); first by apply: sub_setC. move: (iim_fun_C b (canon_proj_f r)). by rewrite aib iim_fun_pr canon_proj_s canon_proj_t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)