proposition: Lemma Exercise6_31_q_bis x: inc x F -> open_o r' (Zo F (gle r' x)).
proof: Proof. move => xF; apply/Exercise6_31_q; split; first by apply: Zo_S. move => t y /Zo_P [tF /Exercise6_31_j /proj33 qa] qb qc. move: (sub_trans qb qa) => qd. have yF: inc y F. move/Zo_P: xF => [/Zo_P [/setP_P xA _] xc]. move: (countable_sub qd xc) => cy. by apply: Zo_i cy; apply:Zo_i qc; apply/setP_P; apply: (sub_trans qd xA). by apply/Zo_P; split => //; apply/Exercise6_31_j. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)