proposition: Lemma Exercise6_31_f x y: inc x inf_subsets -> inc y inf_subsets -> ( (forall t, gle r x t -> gle r y t -> False) <-> finite_set (x \cap y)).
proof: Proof. move => xE yE. split => h. case: (finite_or_infinite_set (x\cap y)) => ixy //. have s1: sub (x \cap y) x by apply: setI2_1. have xyE: inc (x \cap y) inf_subsets. move: (Zo_S xE) => /setP_P xA. apply: Zo_i => //; apply/setP_P; apply: (sub_trans s1 xA). by case: (h (x \cap y)); apply/Exercise6_31_b; split => //; apply: setI2_2. move =>t /Exercise6_31_b [_ /Zo_hi tinf s1] /Exercise6_31_b [_ _ s2]. have txy: sub t (x\cap y). move => s st;apply /setI2_P; split; fprops. exact (finite_not_infinite_set (sub_finite_set txy h) tinf). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)