proposition: Fact char0_ratr_is_additive : additive 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. rewrite /ratr ?divr1 // => 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. by rewrite !numqE (mulrAC y) -!mulrBl -mulrA mulrAC !mulrA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)