(* begin hide *)
(* in this file the concrete canonical isomorphism -in te sense of
R_morphisms.v - between two arbitrary model of real numbers is built *)
(* begin hide *)
(* in this file the concrete canonical isomorphism -in te sense of
R_morphisms.v - between two arbitrary model of real numbers is built *)