proposition: Fact ratr_is_additive : additive (@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. move=> x y. apply: (canLR (mulfK (nz_den _))); apply: (mulIf (nz_den x)). rewrite mulrAC mulrBl divfK ?nz_den // mulrAC -!rmorphM. apply: (mulIf (nz_den y)); rewrite mulrAC mulrBl divfK ?nz_den //. rewrite -!(rmorphM, rmorphB); congr _%:~R; apply: injZtoQ. rewrite !(rmorphM, rmorphB) /= [_ - _]lock /= -lock !numqE. by rewrite (mulrAC y) -!mulrBl -mulrA mulrAC !mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)