proposition: Fact char0_ratr_is_multiplicative : multiplicative ratrF.
proof: Proof. rewrite /char0_ratr. have injZtoQ: @injective rat int intr by apply: intr_inj. have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0. split; rewrite /ratr ?divr1 // => x y. rewrite 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(all_ssreflect all_algebra all_field)