https://github.com/coq-community/corn/blob/af4b86e6ad6cfd242562f9c33c0e438298fc4e1f/coq_reals/Rreals_iso.v#L261
While trying to translate between Coquelicot and corn's complex numbers, I noticed that some of the translations were missing from Rreals_iso.v. Specifically, the translations mapping from IR to R were not present for multiplication, negation, etc... although their corresponding theorems in R_morphism.v exist already. Because the lemmas already exist, it would not be too difficult to add the proofs to Rreals_iso.v and I would be happy to make a pull request.
https://github.com/coq-community/corn/blob/af4b86e6ad6cfd242562f9c33c0e438298fc4e1f/coq_reals/Rreals_iso.v#L261
While trying to translate between Coquelicot and corn's complex numbers, I noticed that some of the translations were missing from Rreals_iso.v. Specifically, the translations mapping from IR to R were not present for multiplication, negation, etc... although their corresponding theorems in R_morphism.v exist already. Because the lemmas already exist, it would not be too difficult to add the proofs to Rreals_iso.v and I would be happy to make a pull request.