proposition: Lemma saturated_setU r x: equivalence r -> (alls x (sub^~ (substrate r))) -> (alls x (saturated r)) -> (sub (union x) (substrate r) /\ saturated r (union x)).
proof: Proof. move=> er als alsa. have r1: (sub (union x) (substrate r)). by move => t /setU_P [z tz zx]; apply: (als _ zx). split=>//;apply /saturatedP => // y /setU_P [z yz zx]. apply: sub_trans (setU_s1 zx). by move: (alsa _ zx) => /(saturatedP er (als _ zx)); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)