proposition: Lemma lowerUpper : forall (f : Q -> bool) (q r : Q), isLowerCut f -> Qle q r -> f q = false -> f r = false.
proof: Proof. intros. destruct H. specialize (H q r H0). destruct (f r) eqn:desR. 2: reflexivity. exfalso. specialize (H (eq_refl _)). rewrite H in H1. discriminate. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra