proposition: Theorem Rmorph_comp (R S : Real.structure) (T : Real.model) (phi : S -> T) (psi : R -> S) : Real.morphism phi -> Real.morphism psi -> Real.morphism (phi \o psi).
proof: Proof. move=> phiP psiP; have [phiR phiPr] := (Rmorph_model phiP, Rmorph_Proper phiP). case: phiR => {S}[S ->] in phi psi phiP phiPr psiP *. split=> /= *; first 2 last. - by rewrite !Real.morph_add. - by rewrite !Real.morph_zero. - by rewrite !Real.morph_opp. - by rewrite !Real.morph_mul. - by rewrite !Real.morph_one. - by rewrite !Real.morph_inv //; apply: Rmorph_neq0. - by rewrite !Real.morph_le. rewrite !Real.morph_sup //; last exact: Rimage_has_sup. set E1 := Real.image phi _; set E2 := Real.image _ _. have eqE12: pointwise_relation T iff E1 E2. by split=> [[_ [x ? ->]] | [x]]; last exists (psi x) => //; exists x. by rewrite -!supRE -?eqE12 //; do 2?apply/Rimage_has_sup. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) Coq(Morphisms Setoid) fourcolor(real realsyntax realprop)