proposition: Lemma FQ : ring_morph 0 1 +%R *%R (fun x y : F => x - y) -%R eq 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool R_of_Q.
proof: Proof. apply: mkmorph. - exact: R_of_Q0. - exact: R_of_Q1. - exact: R_of_Q_add. - exact: R_of_Q_sub. - exact: R_of_Q_mul. - exact: R_of_Q_opp. - by move=> x y; rewrite R_of_Q_eq => /eqP. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)