proposition: Fact ratzD : {morph ratz : x y / x + y >-> addq x y}.
proof: Proof. by move=> x y; rewrite !ratz_frac addq_frac// addq_subdefE/= !mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)