proposition: Lemma separable_le {R : realType} (l1 l2 : \bar R) : (l1 < l2)%E -> exists (v1 : nbh l1) (v2 : nbh l2), forall x y, x \in v1 -> y \in v2 -> x < y.
proof: Proof. case: l1 l2 => [l1||] [l2||] //= lt_l12; last first. + exists (NNInf 0), (NPInf 1) => x y; rewrite !inE => lt1 lt2. by apply/(lt_trans lt1)/(lt_trans ltr01). + exists (NNInf (l2-1)), (B1 l2) => x y; rewrite !inE. rewrite ltr_norml [-1 < _]ltrBrDl. by move => lt1 /andP[lt2 _]; apply/(lt_trans lt1). + exists (B1 l1), (NPInf (l1+1)) => x y; rewrite !inE. rewrite ltr_norml ltrBlDr [1+_]addrC => /andP[_]. by move=> lt1 lt2; apply/(lt_trans lt1). pose e := l2 - l1; exists (B l1 (e/2%:R)), (B l2 (e/2%:R)). have gt0_e: 0 < e by rewrite subr_gt0. move=> x y; rewrite !inE/= /eclamp pmulr_rle0 // invr_le0. rewrite lern0 /= !ltr_distl => /andP[_ lt1] /andP[lt2 _]. apply/(lt_trans lt1)/(le_lt_trans _ lt2). by rewrite lerBrDl addrCA -splitr /e addrCA subrr addr0. 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