proposition: Lemma numqN x : numq (- x) = - numq x.
proof: Proof. rewrite [- _]oppq_def/= num_fracq. case: x => -[a b]; rewrite /numq/= => /andP[b_gt0]. rewrite /coprime => /eqP cab. by rewrite lt_gtF ?gt_eqF // {2}abszN cab divn1 mulz_sign_abs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)