proposition: Lemma LPO_notnotexists : forall P : nat -> Prop, (forall n, P n \/ ~P n) -> ~~ (exists n : nat, P n) -> exists n : nat, P n.
proof: Proof. intros. apply LPO_notforall. apply H. contradict H0. intros (n,H1). contradict H1 ; apply H0. Qed.
imports: Coq(RIneq Lia) Rcomplements