proposition: Lemma Exercise6_31_h: cofinal r F.
proof: Proof. move :Exercise6_31_a =>[or sr]. split; first by rewrite sr; apply: Zo_S. rewrite sr => x xE. move/Zo_P:(xE) => [/setP_P xA ix]. move:(sub_infinite_countable ix) =>[y [ya yb yc]]. have yE: inc y inf_subsets. apply: Zo_i => //; apply/setP_P; apply: (sub_trans yc xA). exists y; first by apply: (Zo_i yE yb). by apply/Exercise6_31_b. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)