proposition: Lemma Zo_exten1 (X : Set) (p q: property): (forall x, inc x X -> (p x <-> q x)) -> Zo X p = Zo X q.
proof: Proof. by move => h; set_extens t => /Zo_P [pa /(h _ pa) pb];apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)