proposition: Lemma Exercise3_6b E: let X:= Zo E (fun t => ~(inc t t)) in sub X E /\ ~ (inc X E).
proof: Proof. move=> U; split;first by apply: Zo_S. move=> UE. have nUU: ~ inc U U by move => h;case: (Zo_hi h). by case: (nUU); apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)