proposition: Fact oppq_frac x : oppq (fracq x) = fracq (oppq_subdef x).
proof: Proof. rewrite /oppq_subdef; case: fracqP => /= [|u fx u_neq0]. by rewrite fracq0. by rewrite oppq_def -mulrN fracqMM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)