proposition: Lemma lowerCutAbove : forall f : Q -> bool, isLowerCut f -> { q : Q | f q = false }.
proof: Proof. intros. destruct (sig_forall_dec (fun n => f (Z.of_nat n # 1)%Q = true)). - intro n. destruct (f (Z.of_nat n # 1)%Q). + left. reflexivity. + right. discriminate. - destruct s. exists (Z.of_nat x # 1)%Q. destruct (f (Z.of_nat x # 1)%Q). + exfalso. apply n. reflexivity. + reflexivity. - exfalso. destruct H, H0, H1. apply H0. intro q. destruct (Qarchimedean q) as [p pmaj]. apply (H q (Z.of_nat (Pos.to_nat p) # 1)%Q). + rewrite positive_nat_Z. apply Qlt_le_weak, pmaj. + apply e. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra