proposition: Lemma RZ (R : ringType) : ring_morph 0 1 +%R *%R (fun x y : R => x - y) -%R eq 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (fun n => (int_of_Z n)%:~R).
proof: Proof. split=> //= [x y | x y | x y | x | x y /Z.eqb_eq -> //]. - by rewrite !rmorphD. - by rewrite !rmorphB. - by rewrite !rmorphM. - by rewrite !rmorphN. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)