proposition: Lemma separable {R : realType} (l1 l2 : \bar R) : l1 != l2 -> exists (v1 : nbh l1) (v2 : nbh l2), forall x, x \notin [predI v1 & v2].
proof: Proof. wlog: l1 l2 / (l1 < l2)%E => [wlog ne_l12|le_l12 _]. case/boolP: (l1 < l2)%E => [/wlog/(_ ne_l12)//|]. rewrite -leNgt le_eqVlt eq_sym (negbTE ne_l12) /=. case/wlog=> [|x [y h]]; first by rewrite eq_sym. by exists y, x=> z; rewrite inE andbC /= (h z). case/separable_le: le_l12 => [v1] [v2] h; exists v1, v2. move=> x; apply/negP; rewrite inE/= => /andP[] xv1 xv2. by have := h _ _ xv1 xv2; rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology