proposition: Lemma set_of_pureP A R x: inc x (set_of_pure A R) <-> (sub x A /\ pure R x).
proof: Proof. split; first by move /Zo_P => [] /setP_P. by move => [pa pb]; apply: Zo_i => //; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)