proposition: Lemma RN (SR : semiRingType) : semi_morph (0 : SR) 1 +%R *%R eq N.zero N.one N.add N.mul N.eqb (fun n => (nat_of_N n)%:R).
proof: Proof. split=> //= [x y | x y | x y]. - by rewrite -natrD; congr _%:R; lia. - by rewrite -natrM; congr _%:R; lia. - by move=> ?; congr _%:R; lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)