proposition: Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
proof: Proof. by move/subnK=> Dm; rewrite -[n in LHS]add0n -[in LHS]Dm eqn_modDr mod0n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)