proposition: Lemma setU_P z x: inc x (union z) <-> exists2 y, inc x y & inc y z.
proof: Proof. split; first by move/setUt_P => [y xr]; exists (Ro y); [ | apply: R_inc]. by move => [y xy yz]; apply/setUt_P; exists (Bo yz); rewrite (B_eq yz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)