proposition: Lemma fracq_opt_subdef_id x : fracq_opt_subdef (fracq_opt_subdef x) = fracq_subdef x.
proof: Proof. rewrite [fracq_opt_subdef (_ x)]/fracq_opt_subdef. by rewrite fracq_subproof fracq_opt_subdefE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)