proposition: Lemma dvdn_eq d m : (d %| m) = (m %/ d * d == m).
proof: Proof. apply/eqP/eqP=> [modm0 | <-]; last exact: modnMl. by rewrite [RHS](divn_eq m d) modm0 addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)