proposition: Lemma dvdCP_nat x y : 0 <= x -> 0 <= y -> (x %| y)%C -> {n | y = n%:R * x}.
proof: Proof. move=> x_ge0 y_ge0 x_dv_y; apply: sig_eqW. case/dvdCP: x_dv_y => z Zz -> in y_ge0 *; move: x_ge0 y_ge0 Zz. rewrite le_eqVlt => /predU1P[<- | ]; first by exists 22%N; rewrite !mulr0. by move=> /pmulr_lge0-> /intrEge0-> /natrP[n ->]; exists n. 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)