proposition: Theorem Rmorph_uniq (S : Real.structure) (R : Real.model) (phi psi : S -> R) : Real.morphism phi -> Real.morphism psi -> pointwise_relation S Real.eq phi psi.
proof: Proof. move=> phiP psiP x. wlog suffices IH: phi psi phiP psiP / phi x <= psi x; first by split; apply: IH. have [//|/ratR_dense[a /ltRW-lexa []]] := reals_classic R (phi x <= psi x). by rewrite -(Rmorph_rat phiP) Real.morph_le // -(Real.morph_le psiP) Rmorph_rat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) Coq(Morphisms Setoid) fourcolor(real realsyntax realprop)