proposition: Lemma Zo_P x (p: property) y: inc y (Zo x p) <-> (inc y x /\ p y).
proof: Proof. split=> [H | [u v]]; last by apply: Zo_i. split; [ exact: (Zo_S H) | exact: (Zo_hi H) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)