proposition: Lemma Rle_antisym : forall x y : DReal, Rle x y -> Rle y x -> x = y.
proof: Proof. intros [f cf] [g cg] H H0. unfold Rle in H,H0; simpl in H, H0. assert (f = g). { apply functional_extensionality. intro q. specialize (H q). specialize (H0 q). destruct (f q), (g q). - reflexivity. - exfalso. specialize (H (eq_refl _)). discriminate. - exfalso. specialize (H0 (eq_refl _)). discriminate. - reflexivity. } subst g. replace cg with cf. - reflexivity. - apply isLowerCut_hprop. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra