proposition: Lemma R_of_Q_mul (F : fieldType) x y : R_of_Q (x * y) = R_of_Q x * R_of_Q y :> F.
proof: Proof. by rewrite /R_of_Q /= mulrACA -invfM -intrM -natrM; congr (_%:~R / _%:R); lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)