proposition: Lemma Rmorph_int m : phi (intR R m) == intR S m.
proof: Proof. by case: m => n; rewrite ?phiN Rmorph_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) Coq(Morphisms Setoid) fourcolor(real realsyntax realprop)