proposition: Lemma UpperAboveLower : forall (f : Q -> bool) (q r : Q), isLowerCut f -> f q = true -> f r = false -> Qlt q r.
proof: Proof. intros. destruct H. apply Qnot_le_lt. intro abs. rewrite (H r q abs) in H1. - discriminate. - exact H0. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra