proposition: Theorem Rmorph_to_id (R : Real.model) x : Rmorph_to R x == x.
proof: Proof. exact: Rmorph_uniq (Rmorph_toP R R) (Rmorph_id R) x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) Coq(Morphisms Setoid) fourcolor(real realsyntax realprop)