proposition: Lemma dvdC_nat (p n : nat) : (p %| n)%C = (p %| n)%N.
proof: Proof. rewrite unfold_in intrEge0 ?divr_ge0 ?invr_ge0 ?ler0n // !pnatr_eq0. have [-> | nz_p] := eqVneq; first by rewrite dvd0n. apply/natrP/dvdnP=> [[q def_q] | [q ->]]; exists q. by apply/eqP; rewrite -eqC_nat natrM -def_q divfK ?pnatr_eq0. by rewrite [num in num / _]natrM mulfK ?pnatr_eq0. 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)