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