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