proposition: Lemma mod_eq0 a b : (a %% b == 0) = (b %| a).
proof: Proof. case: (edivP a b)=> q r -> /=. have [-> | /= b0] := eqVneq b 0; first by rewrite mulr0 dvd0r add0r. move=> nrb; apply/eqP/idP=> [->|]. by apply/dvdrP; exists q; rewrite addr0. rewrite dvdr_addr ?dvdr_mull //. have [-> // | r0] := eqVneq r 0. by move/leq_norm; rewrite leqNgt r0 nrb => /(_ isT). Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete