proposition: Lemma isLowerCut_hprop : forall (f : Q -> bool), IsHProp (isLowerCut f).
proof: Proof. intro f. apply and_hprop. 2: apply and_hprop. 2: apply not_hprop. 2: apply and_hprop. 2: apply not_hprop. - apply forall_hprop. intro x. apply forall_hprop. intro y. apply impl_hprop. apply impl_hprop. intros p q. apply eq_proofs_unicity_on. intro b. destruct (f x), b. + left. reflexivity. + right. discriminate. + right. discriminate. + left. reflexivity. - apply forall_hprop. intro q. apply impl_hprop. apply not_hprop. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra