fact: Definition isLowerCut (f : Q -> bool) : Prop := (forall q r:Q, Qle q r -> f r = true -> f q = true) /\ ~(forall q:Q, f q = true) /\ ~(forall q:Q, f q = false) /\ (forall q:Q, f q = true -> ~(forall r:Q, Qle r q \/ f r = false)).
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra