proposition: Lemma CReal_of_DReal_seq_max_prec_1 : forall (x : DReal) (n : Z), (n>=0)%Z -> CReal_of_DReal_seq x n = CReal_of_DReal_seq x 0.
proof: Proof. intros x n Hngt0. unfold CReal_of_DReal_seq. destruct n. - reflexivity. - reflexivity. - lia. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra