proposition: Lemma Exercise6_31_j_bis x y: inc x F -> infinite_set y -> sub y x -> gle r' x y.
proof: Proof. move => xF yi syx. move /Zo_P: (xF) => [/Zo_P [/setP_P xA xi] xc]. have yF: inc y F. apply: Zo_i (countable_sub syx xc); apply: Zo_i yi. apply/setP_P; apply: (sub_trans syx xA). by apply/Exercise6_31_j. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)