proposition: Lemma Rmorph_nat n : phi n%:R == n%:R.
proof: Proof. by case: n; [apply: phi0 | elim=> //= n IHn; rewrite phiD phi1 IHn]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) Coq(Morphisms Setoid) fourcolor(real realsyntax realprop)