proposition: Lemma Exercise6_31_q U: open_o r' U <-> sub U F /\ forall x y, inc x U -> sub y x -> infinite_set y -> inc y U.
proof: Proof. move: Exercise6_31_i => [pr sr]. split. move=> [qa qb]; split; [ by rewrite - sr | move => x y xU syx ict]. move: (qa _ xU); rewrite sr => xF. apply: (qb _ _ xU); apply/Exercise6_31_j; split => //. move/Zo_P: xF => [/Zo_P [/setP_P xA xi] xc]. have ya: inc y (\Po A). apply/setP_P; apply: (sub_trans syx xA). by apply: Zo_i (countable_sub syx xc); apply/Zo_i. move =>[qa qb]; split; [ by rewrite sr | move => x y xU /Exercise6_31_j]. by move => [xF /Zo_S /Zo_hi h sxy]; apply: (qb _ _ xU sxy). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)