proposition: Fact getCrat_subproof : getCrat_spec.
proof: Proof. have isQ := rat_algebraic_decidable algebraic. exists (fun z => if isQ z is left Qz then sval (sig_eqW Qz) else 0) => a. case: (isQ _) => [Qa | []]; last by exists a. by case: (sig_eqW _) => b /= /fmorph_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)