Coq's classical real numbers imply the weak law of excluded middle

RealLEM.v

Require Import Reals.

Definition WeakLEM := forall (P : Prop), {~~P} + {~P}.

Local Open Scope R_scope.

Definition ind (P : Prop) (x : R) : Prop :=
  (x = 0) \/ (x = 1 /\ P).


Definition sup_of_ind (P : Prop) 
  : { m : R | is_lub (ind P) m }.
Proof.
apply completeness.
unfold bound. exists 1. unfold is_upper_bound.
unfold ind. intros. destruct H.
- subst. apply Rle_0_1.
- destruct H. subst. apply Rle_refl.
- exists 0. unfold ind. left. reflexivity.
Qed.

Theorem classical : WeakLEM.
Proof.
unfold WeakLEM. intros.
destruct (sup_of_ind P).
unfold is_lub in i.
destruct i as (upper & least).
destruct (Rle_lt_dec x 0) as [LE | GT].
- right. unfold not. intros.
  specialize (upper 1). 
  apply (Rle_not_lt x 1). apply upper. 
  unfold ind. right. split. reflexivity. 
  assumption.
  eapply Rle_lt_trans. eassumption. apply Rlt_0_1.
- left. unfold not. intros.
  apply (Rle_not_lt 0 x).
  apply least. unfold is_upper_bound.
  intros y Hy. destruct Hy. subst. apply Rle_refl.
  destruct H0. contradiction. assumption.
Qed.

Print Assumptions classical.