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