proposition: Fact addq_frac x y : x.2 != 0 -> y.2 != 0 -> (addq (fracq x) (fracq y)) = fracq (addq_subdef x y).
proof: Proof. case: fracqP => // u fx u_neq0 _; case: fracqP => // v fy v_neq0 _. rewrite addq_def !addq_subdefE /=. rewrite ![(_ * numq _) * _]mulrACA [(_ * denq _) * _]mulrACA. by rewrite [v * _]mulrC -mulrDr fracqMM ?mulf_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)