proposition: Lemma R_of_Q_add (F : numFieldType) x y : R_of_Q (x + y) = R_of_Q x + R_of_Q y :> F.
proof: Proof. rewrite /R_of_Q /= addf_div ?pnatr_eq0; try lia. by rewrite !pmulrn -!intrM -!intrD; congr (_%:~R / _%:~R); lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)