proposition: Lemma dvdnP m n : reflect (Z.divide (Z.of_nat m) (Z.of_nat n)) (m %| n).
proof: Proof. apply: (iffP idP) => H. { rewrite dvdn_eq in H; rewrite -(eqP H) /Z.divide; exists (Z.of_nat (n %/ m)). by rewrite Nat2Z.inj_mul. } { have [q Hq] := H; apply/dvdnP; exists `|Z2int q|%N; apply/Nat2Z.inj. have [Zq|NZq] := Z_zerop q. { by rewrite Zq /= in Hq *. } case: m Hq H => [|m] Hq H. { by rewrite Zmult_comm /= in Hq; rewrite mulnC /=. } rewrite Nat2Z.inj_mul -Zabs_natE Zabs2Nat.id_abs Z.abs_eq //. have H0 : (0 <= q * Z.of_nat m.+1) by rewrite -Hq; apply Zle_0_nat. by apply: Zmult_le_0_reg_r H0. } Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)