proposition: Fact ratr_is_multiplicative : multiplicative (@ratr F).
proof: Proof. have injZtoQ: @injective rat int intr by apply: intr_inj. have nz_den x: (denq x)%:~R != 0 :> F by rewrite intr_eq0 denq_eq0. split=> [x y|]; last by rewrite /ratr divr1. rewrite /ratr mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA. do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R. apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock. by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)