proposition: Lemma rat_field_theory : Field_theory.field_theory 0%Q 1%Q addq mulq subq oppq divq invq eq.
proof: Proof. split => //; first exact: rat_ring_theory. by move=> p /eqP p_neq0; rat_to_ring; rewrite mulVf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)