proposition: Lemma R_rm : ring_morph 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.
proof: Proof. constructor; try easy. - exact plus_IZR. - exact minus_IZR. - exact mult_IZR. - exact opp_IZR. - now intros x y H; f_equal; apply Zeq_bool_eq. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField