proposition: Lemma rat_ring_theory : (ring_theory 0%Q 1%Q addq mulq subq oppq eq).
proof: Proof. split => * //; rat_to_ring; by rewrite ?(add0r, addrA, mul1r, mulrA, mulrDl, subrr) // (addrC, mulrC). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)