fact: Definition CintrE := let CnF : numClosedFieldType := algC in let ZtoCm : {rmorphism _ -> _} := *~%R (1 : CnF) in ((rmorph0 ZtoCm, rmorph1 ZtoCm, rmorphMn ZtoCm, rmorphN ZtoCm, rmorphD ZtoCm), (rmorphM ZtoCm, rmorphXn ZtoCm), (rmorphMz ZtoCm, @intr_norm CnF, @intr_sg CnF), =^~ (@ler_int CnF, @ltr_int CnF, (inj_eq (@intr_inj CnF)))).
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)