fact: Record Isomorphism : Type := {iso_map_lft : Homomorphism R1 R2; iso_map_rht : Homomorphism R2 R1; inversity_lft : map_is_id R2 (Compose R2 R1 R2 iso_map_rht iso_map_lft); inversity_rht : map_is_id R1 (Compose R1 R2 R1 iso_map_lft iso_map_rht)}.
imports: CoRN.reals.CReals