proposition: Lemma DRealQuot1 : forall x y:DReal, CRealEq (DRealRepr x) (DRealRepr y) -> x = y.
proof: Proof. intros. destruct H. apply Rle_antisym. - clear H. intros q H1. destruct (proj1_sig y q) eqn:des. + reflexivity. + exfalso. apply H0. apply (CReal_le_lt_trans _ (inject_Q q)). * apply DRealReprQup. exact des. * apply DRealReprQ. exact H1. - clear H0. intros q H1. destruct (proj1_sig x q) eqn:des. + reflexivity. + exfalso. apply H. apply (CReal_le_lt_trans _ (inject_Q q)). * apply DRealReprQup. exact des. * apply DRealReprQ. exact H1. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra