proposition: Lemma f12_inverse_lft : map_is_id R2 (Compose R2 R1 R2 g21_as_Homomorphism f12_as_Homomorphism).
proof: Proof. red in |- *. intros. simpl in |- *. apply eq_symmetric_unfolded. apply f12_is_inverse_g21. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism