proposition: Lemma fracq_opt_subdefE x : fracq_opt_subdef x = fracq_subdef x.
proof: Proof. rewrite /fracq_opt_subdef; case: ifP => //; case: x => n d /= /andP[d_gt0 cnd]. rewrite /fracq_subdef gt_eqF//= lt_gtF//= (eqP cnd) !divn1 abszEsg gtz0_abs//. rewrite mulrA sgz_def mulrnAr -signr_addb addbb expr0. by have [->|] := eqVneq n 0; rewrite (mulr0, mul1r). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)